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 program
Proceedings of the First International Workshop on Verification and Program Transformation
Saint Petersburg, Russia
2013
first
Lisitsa, A.; Nemytykh, A.
Rilevanza internazionale
su invito
13-lug-2013
lug-2013
Settore ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
English
Intervento a convegno
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.
Pettorossi, A; Proietti, M
File in questo prodotto:
File 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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2108/81889
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact