Model checking procedural programs

Rajeev Alur, Ahmed Bouajjani, Javier Esparza

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

13 Scopus citations


We consider the model-checking problem for sequential programs with procedure calls. We first present basic algorithms for solving the reachability problem and the fair computation problem. The algorithms are based on two techniques: summarization, which computes reachability information by solving a set of fixpoint equations, and saturation, which computes the set of all reachable program states (including call stacks) using automata. Then, we study formalisms to specify requirements of programs with procedure calls. We present an extension of Linear Temporal Logic allowing propagation of information across the hierarchical structure induced by procedure calls and matching returns. Finally, we show how model checking can be extended to this class of programs and properties.

Original languageEnglish
Title of host publicationHandbook of Model Checking
PublisherSpringer International Publishing
Number of pages32
ISBN (Electronic)9783319105758
ISBN (Print)9783319105741
StatePublished - 18 May 2018


Dive into the research topics of 'Model checking procedural programs'. Together they form a unique fingerprint.

Cite this