Compositional verification of sequential programs with procedures

Dilian Gurov, Marieke Huisman, Christoph Sprenger

Research output: Contribution to journalArticleAcademicpeer-review

18 Citations (Scopus)


We present a method for algorithmic, compositional verification of control-flow-based safety properties of sequential programs with procedures. The application of the method involves three steps: (1) decomposing the desired global property into local properties of the components, (2) proving the correctness of the property decomposition by using a maximal model construction, and (3) verifying that the component implementations obey their local specifications. We consider safety properties of both the structure and the behaviour of program control flow. Our compositional verification method builds on a technique proposed by Grumberg and Long that uses maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. We present a novel maximal model construction for the fragment of the modal μ-calculus with boxes and greatest fixed points only, and adapt it to control-flow graphs modelling components described in a sequential procedural language. We extend our verification method to programs with private procedures by defining an abstraction, presented as an inlining transformation. All algorithms have been implemented in a tool set automating all required verification steps. We validate our approach on an electronic purse case study.
Original languageEnglish
Pages (from-to)840-868
Number of pages29
JournalInformation and computation
Issue number7
Publication statusPublished - 2008
Externally publishedYes


  • Program verification
  • Control-flow behaviour
  • Compositional reasoning
  • Modal μ-calculus
  • Safety properties
  • Maximal model
  • Private procedures


Dive into the research topics of 'Compositional verification of sequential programs with procedures'. Together they form a unique fingerprint.

Cite this