Change search
ReferencesLink to record
Permanent link

Direct link
Compositional verification of sequential programs with procedures
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2008 (English)In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 206, no 7, 840-868 p.Article in journal (Refereed) Published
Abstract [en]

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 P-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.

Place, publisher, year, edition, pages
2008. Vol. 206, no 7, 840-868 p.
Keyword [en]
program verification, control-flow behaviour, compositional reasoning, modal mu-calculus, safety properties, maximal model, private procedures, modular model checking, reachability analysis, applet interactions, software, automata, machines
URN: urn:nbn:se:kth:diva-17733DOI: 10.1016/j.ic.2008.03.003ISI: 000258015900004ScopusID: 2-s2.0-46149087012OAI: diva2:335778
QC 20100525Available from: 2010-08-05 Created: 2010-08-05Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Gurov, Dilian
By organisation
Theoretical Computer Science, TCS
In the same journal
Information and Computation

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 30 hits
ReferencesLink to record
Permanent link

Direct link