Skip to main content
Model checking REcursive programs with COUNTers

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.

Faculty

Past Members

Selected Publications

View All