Change search
ReferencesLink to record
Permanent link

Direct link
Reducing Behavioural to Structural Properties of Programs with Procedures
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
University of Twente, Netherlands.
2009 (English)In: VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION / [ed] Jones ND; MullerOlm M, 2009, Vol. 5403, 136-150 p.Conference paper (Refereed)
Abstract [en]

There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. This paper presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with possibly recursive procedures, and properties expressed in a fragment of the modal mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. We discuss several applications of the characterisation, in particular compositional verification for behavioural properties, based on maximal models.

Place, publisher, year, edition, pages
2009. Vol. 5403, 136-150 p.
Keyword [en]
Abstracting, Concurrency control, Model checking, Program interpreters, Program translators, Software prototyping, Translation (languages), Characterisation, Control flow graph (CFG), Program correctness, Program properties, Program structures, Prototype implementations, Recursion
National Category
Computer Science
URN: urn:nbn:se:kth:diva-31214DOI: 10.1007/978-3-540-93900-9_14ISI: 000264750800010ScopusID: 2-s2.0-58449092934ISBN: 978-3-540-93899-6OAI: diva2:406254
10th International Conference on Verification, Model Checking and Abstract Interpretation, Savannah, GA, JAN 18-20, 2009
QC 20110325Available from: 2011-03-25 Created: 2011-03-11 Last updated: 2011-03-25Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Gurov, DilianHuisman, Marieke
By organisation
Theoretical Computer Science, TCS
Computer Science

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: 24 hits
ReferencesLink to record
Permanent link

Direct link