Model checking REcursive programs with COUNTers

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.

Selected Publications

View All

• Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters

  Matthew Hague and Anthony Widjaja Lin

  In Computer Aided Verification (CAV), 2012.

  Details about Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters | BibTeX data for Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters | Download  (pdf) of Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters

• Model Checking Recursive Programs with Numeric Data Types

  Matthew Hague and Anthony Widjaja Lin

  In Computer Aided Verification (CAV). 2011.

  Prototypical implementation: [tgz] [txz].

  Details about Model Checking Recursive Programs with Numeric Data Types | BibTeX data for Model Checking Recursive Programs with Numeric Data Types | Download  (pdf) of Model Checking Recursive Programs with Numeric Data Types