Reducing Behavioural to Structural Properties of Programs with Procedures

Dilian Gurov, Marieke Huisman

Research output: Contribution to journalArticleAcademicpeer-review

1 Citation (Scopus)
7 Downloads (Pure)

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. 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.
Original languageUndefined
Pages (from-to)69-103
Number of pages35
JournalTheoretical computer science
Volume480
DOIs
Publication statusPublished - 8 Apr 2013

Keywords

  • EWI-23277
  • Safety properties
  • Program Verification
  • Compositional reasoning
  • IR-85832
  • Control-flow behaviour
  • Control-flow structure
  • METIS-296403
  • Modal mu-calculus

Cite this

@article{4a0138d5e3504e518cd5e23edc156c18,
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. 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.",
keywords = "EWI-23277, Safety properties, Program Verification, Compositional reasoning, IR-85832, Control-flow behaviour, Control-flow structure, METIS-296403, Modal mu-calculus",
author = "Dilian Gurov and Marieke Huisman",
note = "eemcs-eprint-23277",
year = "2013",
month = "4",
day = "8",
doi = "10.1016/j.tcs.2013.02.006",
language = "Undefined",
volume = "480",
pages = "69--103",
journal = "Theoretical computer science",
issn = "0304-3975",
publisher = "Elsevier",

}

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

In: Theoretical computer science, Vol. 480, 08.04.2013, p. 69-103.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Reducing Behavioural to Structural Properties of Programs with Procedures

AU - Gurov, Dilian

AU - Huisman, Marieke

N1 - eemcs-eprint-23277

PY - 2013/4/8

Y1 - 2013/4/8

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

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

KW - EWI-23277

KW - Safety properties

KW - Program Verification

KW - Compositional reasoning

KW - IR-85832

KW - Control-flow behaviour

KW - Control-flow structure

KW - METIS-296403

KW - Modal mu-calculus

U2 - 10.1016/j.tcs.2013.02.006

DO - 10.1016/j.tcs.2013.02.006

M3 - Article

VL - 480

SP - 69

EP - 103

JO - Theoretical computer science

JF - Theoretical computer science

SN - 0304-3975

ER -