Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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 .
2013 (English)In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 480, 69-103 p.Article in journal (Refereed) Published
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. The present 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 procedures, abstracting away completely from program data, 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. In addition, we show how the translation can be extended beyond the basic flow graph model and safety logic to richer behavioural models (such as open programs) and richer program models (including Boolean programs), and discuss possible extensions for more complex logics. We present several applications of the characterisation, in particular sound and complete compositional verification for behavioural properties based on maximal models.

Place, publisher, year, edition, pages
2013. Vol. 480, 69-103 p.
Keyword [en]
Compositional reasoning, Control-flow behaviour, Control-flow structure, Modal mu-calculus, Program verification, Safety properties
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-122330DOI: 10.1016/j.tcs.2013.02.006ISI: 000317700600004Scopus ID: 2-s2.0-84875518346OAI: oai:DiVA.org:kth-122330DiVA: diva2:622479
Funder
EU, European Research Council, IST-FP6-STREP-27004 S3MS IST-2005-015905 MOBIUS
Note

QC 20130522

Available from: 2013-05-22 Created: 2013-05-20 Last updated: 2017-12-06Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Gurov, Dilian

Search in DiVA

By author/editor
Gurov, DilianHuisman, Marieke
By organisation
Theoretical Computer Science, TCS
In the same journal
Theoretical Computer Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 58 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf