[an error occurred while processing this directive]<title>Department of Computer Science: Model checking REcursive programs with COUNTers</title>
<meta name="keywords"
      content="Department of Computer Science Research Activities Model checking REcursive programs with COUNTers"></meta>
<meta name="description"
      content="Research activities in the area of Model checking REcursive programs with COUNTers"></meta>
<meta property="og:site_name" content="Department of Computer Science"></meta>
<meta property="og:title" content="Model checking REcursive programs with COUNTers"></meta>
<meta property="og:image"
      content="http://www.cs.ox.ac.uk/images/CompSci_logo_landscapeL_rgb_corrected.jpg"></meta>
<meta property="og:url" content="http://www.cs.ox.ac.uk/activities/RECOUNT/"></meta>
[an error occurred while processing this directive]
<!-- BREADCRUMBS -->
<div class="content-width">
   <ol class="breadcrumb text-uppercase">
      <li>
         <a href="/">Home</a>
      </li>
      <li>
         <a href="/research/">Research</a>
      </li>
      <li>
         <a href="/research/verification/">Automated Verification</a>
      </li>
      <li>
         <a href="/research/verification/activities.html">activities</a>
      </li>
      <li class="active">Model checking REcursive programs with COUNTers</li>
   </ol>
</div>
<!-- MOBILE NAVIGATION -->
<div class="content-width space-below mobile-menu-placeholder visible-xs visible-sm"></div>
<!-- COLUMNS -->
<div class="container-fluid content-width">
   <div class="row">
      <div class="col-xs-12 col-md-6 col-md-push-3" id="maincontent">
         <div class="page-title">
            <div class="row">
               <div class="col-xs-12 col-md-7 space-below">
                  <img class="img-responsive" src="/files/4043/recount.jpg"
                       alt="Model checking REcursive programs with COUNTers"></img>
               </div>
            </div>
            <div class="row">
               <div class="col-xs-12 col-md-12">
                  <h1>Model checking REcursive programs with COUNTers</h1>
               </div>
            </div>
         </div><p>Recursions arise naturally when writing programs. They can be naturally  modeled by programs with one stack, a.k.a., pushdown
         systems. At the  same time, numeric data types are abundant in real-world programs. This  project aims to study the extension
         of pushdown systems with unbounded  counters, which naturally model numeric data types. Through techniques  such as reversal-bounded
         model checking, we aim to develop practical  tools and techniques for verifying recursive programs with numeric data  types.</p>
         <div class="row">
            <h3>Past Members</h3>
         </div>
         <div class="row">
            <div itemscope="itemscope" itemtype="http://schema.org/Person"
                 class="picturebox col-xs-6 col-sm-4 col-md-4  clear-xs clear-sm clear-md clear-lg">
               <a class="piccy" style="background-image:url('/files/180//IMG_9155thumb.jpg')"></a>
               <center>
                  <span class="newcaption">
                     <span itemprop="name">Matthew Hague</span>
                  </span>
               </center>
            </div>
            <div itemscope="itemscope" itemtype="http://schema.org/Person"
                 class="picturebox col-xs-6 col-sm-4 col-md-4 ">
               <a class="piccy" style="background-image:url('/files/3576//anthony.to.gif')"></a>
               <center>
                  <span class="newcaption">
                     <span itemprop="name">Anthony W. Lin</span>
                  </span>
               </center>
            </div>
         </div>
         <h2>Selected Publications</h2>
         <p>
            <a href="/activities/publications/date/RECOUNT.html"
               class="btn btn-dark-brown-outline btn-thin text-uppercase">View All</a>
         </p>
         <ul class="list-unbulleted list-unbulleted-spaced"><li> <p class="publicationTitle"> <strong>
            Synchronisation&#x2212; and Reversal&#x2212;Bounded Analysis of Multithreaded Programs with Counters </strong> </p>
            	    <p class="publicationAuthors"> <em> Matthew Hague and Anthony Widjaja Lin  </em> </p>
            	
            	
            	<p class="publicationDetails"> In Computer Aided Verification (CAV), 2012.
            </p>
            	
            <p class="publicationlinks"> <a
            
            href="/publications/publication6000-abstract.html"> Details   <span class="sr-only" > about <em> Synchronisation&#x2212; and
            Reversal&#x2212;Bounded Analysis of Multithreaded Programs with Counters  </em></span> </a> | <a
            
            href="/publications/publication6000.bib"> BibTeX  <span class="sr-only" > data for <em> Synchronisation&#x2212; and Reversal&#x2212;Bounded
            Analysis of Multithreaded Programs with Counters  </em></span>   </a> 
            	    
            	     |
            <a 
            href="http://www.cs.ox.ac.uk/files/4779/cav12.pdf">Download
            		     (pdf)
            		    
            		    <span class="sr-only" > of <em> Synchronisation&#x2212; and Reversal&#x2212;Bounded Analysis of Multithreaded Programs
            with Counters  </em></span>
            		    
            		    </a>
            		
            		
            	    </li><li> <p class="publicationTitle"> <strong>
            Model Checking Recursive Programs with Numeric Data Types </strong> </p>
            	    <p class="publicationAuthors"> <em> Matthew Hague and Anthony Widjaja Lin  </em> </p>
            	
            	
            	<p class="publicationDetails"> 
            In  
            <em>
            Computer Aided Verification (CAV)</em>.
            2011.
            </p> <p
            class="publicationNote"> Prototypical implementation: <a href="http://www.comlab.ox.ac.uk/recount/downloads/implementation.tgz">[tgz]</a>
            <a href="http://www.comlab.ox.ac.uk/recount/downloads/implementation.txz">[txz]</a>.</p>
            	
            <p class="publicationlinks"> <a
            
            href="/publications/publication4910-abstract.html"> Details   <span class="sr-only" > about <em> Model Checking Recursive
            Programs with Numeric Data Types  </em></span> </a> | <a
            
            href="/publications/publication4910.bib"> BibTeX  <span class="sr-only" > data for <em> Model Checking Recursive Programs
            with Numeric Data Types  </em></span>   </a> 
            	    
            	     |
            <a 
            href="http://www.cs.ox.ac.uk/files/3952/cav11-full.pdf">Download
            		     (pdf)
            		    
            		    <span class="sr-only" > of <em> Model Checking Recursive Programs with Numeric Data Types  </em></span>
            		    
            		    </a>
            		
            		
            	    </li>
         </ul>
         <div class="row"></div>
      </div>
      <!-- TACTICAL BOXES (Column 3) -->
      <div class="col-xs-12 col-md-3 col-md-push-3 no-print">
         <div class="row">
            <div class="col-xs-12 col-sm-6 col-md-12">
               <div class="panel panel-dark-brown panel-links text-center">
                  <div class="panel-heading clearfix">
                     <h2 class="panel-title panel-title-small text-uppercase">See also</h2>
                     <span class="underbar"></span>
                  </div>
                  <div class="panel-body no-top-padding">
                     <ul>
                        <li style="margin-bottom:0.33em">
                           <a href="/research/verification">Automated Verification</a>
                        </li>
                     </ul>
                  </div>
               </div>
            </div>
         </div>
      </div>
      <div class="col-xs-12 col-md-3 col-md-pull-9 side-menu-col">
         <!-- NAVIGATION (Column 1) -->
         [an error occurred while processing this directive]
      </div>
   </div>
</div>
[an error occurred while processing this directive]