Reducing Behavioural to Structural Properties of Programs with Procedures

D. Gurov, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
EditorsN.D. Jones, M. Müller-Olm
Place of PublicationLondon
PublisherSpringer
Pages136-150
Number of pages15
ISBN (Print)978-3-540-93899-6
DOIs
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume5403

Fingerprint

Structural properties
Flow graphs
Acoustic waves

Keywords

  • Property translation
  • Compositional verification
  • Temporal Logic

Cite this

Gurov, D., & Huisman, M. (2009). Reducing Behavioural to Structural Properties of Programs with Procedures. In N. D. Jones, & M. Müller-Olm (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 136-150). [10.1007/978-3-540-93900-9_14] (Lecture Notes in Computer Science; Vol. 5403). London: Springer. https://doi.org/10.1007/978-3-540-93900-9_14
Gurov, D. ; Huisman, Marieke. / Reducing Behavioural to Structural Properties of Programs with Procedures. Verification, Model Checking, and Abstract Interpretation. editor / N.D. Jones ; M. Müller-Olm. London : Springer, 2009. pp. 136-150 (Lecture Notes in Computer Science).
@inproceedings{83c8cbf9bb5248b0b577f09011162956,
title = "Reducing Behavioural to Structural Properties of Programs with Procedures",
abstract = "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.",
keywords = "Property translation, Compositional verification, Temporal Logic",
author = "D. Gurov and Marieke Huisman",
year = "2009",
doi = "10.1007/978-3-540-93900-9_14",
language = "English",
isbn = "978-3-540-93899-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "136--150",
editor = "N.D. Jones and M. M{\"u}ller-Olm",
booktitle = "Verification, Model Checking, and Abstract Interpretation",

}

Gurov, D & Huisman, M 2009, Reducing Behavioural to Structural Properties of Programs with Procedures. in ND Jones & M Müller-Olm (eds), Verification, Model Checking, and Abstract Interpretation., 10.1007/978-3-540-93900-9_14, Lecture Notes in Computer Science, vol. 5403, Springer, London, pp. 136-150. https://doi.org/10.1007/978-3-540-93900-9_14

Reducing Behavioural to Structural Properties of Programs with Procedures. / Gurov, D.; Huisman, Marieke.

Verification, Model Checking, and Abstract Interpretation. ed. / N.D. Jones; M. Müller-Olm. London : Springer, 2009. p. 136-150 10.1007/978-3-540-93900-9_14 (Lecture Notes in Computer Science; Vol. 5403).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Reducing Behavioural to Structural Properties of Programs with Procedures

AU - Gurov, D.

AU - Huisman, Marieke

PY - 2009

Y1 - 2009

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

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

KW - Property translation

KW - Compositional verification

KW - Temporal Logic

U2 - 10.1007/978-3-540-93900-9_14

DO - 10.1007/978-3-540-93900-9_14

M3 - Conference contribution

SN - 978-3-540-93899-6

T3 - Lecture Notes in Computer Science

SP - 136

EP - 150

BT - Verification, Model Checking, and Abstract Interpretation

A2 - Jones, N.D.

A2 - Müller-Olm, M.

PB - Springer

CY - London

ER -

Gurov D, Huisman M. Reducing Behavioural to Structural Properties of Programs with Procedures. In Jones ND, Müller-Olm M, editors, Verification, Model Checking, and Abstract Interpretation. London: Springer. 2009. p. 136-150. 10.1007/978-3-540-93900-9_14. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-93900-9_14