We present a transformational approach to program verification and software model checking that uses three main ingredients: (i) Constraint Logic Programming (CLP), (ii) metaprogram- ming and program specialization, and (iii) proof by transformation. (i) Constraints are used for representing in a compact way (finite or infinite) sets of values or memory states, and logic is used for expressing properties of program executions [2, 4, 5]. The least fixpoint semantics and negation allow us to denote both the least models and the greatest models of programs, and thus to reason about the (finite or infinite) behaviour of programs. (ii) Metaprogramming is used for getting a verification technique which is parametric with respect to the programming language in use. In particular, we introduce a CLP program I which defines the (meta)interpreter of the programming language in which the program P to be verified is written. Then, in order to gain efficiency, we remove this interpretation layer by specializing the interpreter I with respect to the given program P [1, 6, 7]. The property φ that should be proved (or disproved) about program P , is expressed through the CLP clauses that characterize the set of states in which φ holds (or does not hold, respectively). (iii) Having derived a CLP program
Pettorossi, A., Proietti, M. (2013). Program transformation for program verification. In Proceedings of the First International Workshop on Verification and Program Transformation (VPT) (pp.116-117). Saint Petersburg : Ailamazyan Program Systems Institute of RAS.
Program transformation for program verification
PETTOROSSI, ALBERTO;
2013-07-01
Abstract
We present a transformational approach to program verification and software model checking that uses three main ingredients: (i) Constraint Logic Programming (CLP), (ii) metaprogram- ming and program specialization, and (iii) proof by transformation. (i) Constraints are used for representing in a compact way (finite or infinite) sets of values or memory states, and logic is used for expressing properties of program executions [2, 4, 5]. The least fixpoint semantics and negation allow us to denote both the least models and the greatest models of programs, and thus to reason about the (finite or infinite) behaviour of programs. (ii) Metaprogramming is used for getting a verification technique which is parametric with respect to the programming language in use. In particular, we introduce a CLP program I which defines the (meta)interpreter of the programming language in which the program P to be verified is written. Then, in order to gain efficiency, we remove this interpretation layer by specializing the interpreter I with respect to the given program P [1, 6, 7]. The property φ that should be proved (or disproved) about program P , is expressed through the CLP clauses that characterize the set of states in which φ holds (or does not hold, respectively). (iii) Having derived a CLP programFile | Dimensione | Formato | |
---|---|---|---|
13-VPT_Invited.pdf
accesso aperto
Descrizione: Abstract
Dimensione
54 kB
Formato
Adobe PDF
|
54 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.