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.
People
|
Research |
|
|
Past Members |
|
Selected Publications
| Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters Matthew Hague and Anthony Widjaja Lin In Computer Aided Verification (CAV), 2012. |
| Model Checking Recursive Programs with Numeric Data Types Matthew Hague and Anthony Widjaja Lin In Computer Aided Verification (CAV). 2011. |
Info
|
Themes |
