We present a method for verifying relational program properties, that is, properties that relate the input and the output of two programs. Our verification method is parametric with respect to the definition of the operational semantics of the programming language in which the two programs are written. That definition of the semantics consists of a set Int of constrained Horn clauses (CHCs) that encode the interpreter of the programming language. Then, given the programs and the relational property we want to verify, we generate, by using Int, a set of constrained Horn clauses whose satisfiability is equivalent to the validity of the property. Unfortunately, state-of-the-art solvers for CHCs have severe limitations in proving the satisfiability, or the unsatisfiability, of such sets of clauses. We propose some transformation techniques that increase the power of CHC solvers when verifying relational properties. We show that these transformations, based on unfold/fold rules, preserve satisfiability. Through an experimental evaluation, we show that in many cases CHC solvers are able to prove the satisfiability (or the unsatisfi- ability) of sets of clauses obtained by applying the transformations we propose, whereas the same solvers are unable to perform those proofs when given as input the original, untransformed sets of CHCs.

De Angelis, E., Fioravanti, F., Pettorossi, A., & Proietti, M. (2016). Relational verification through horn clause transformation. In Static analysis: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016: proceedings (pp.147-169). Springer Verlag [10.1007/978-3-662-53413-7_8].

Relational verification through horn clause transformation

PETTOROSSI, ALBERTO;
2016

Abstract

We present a method for verifying relational program properties, that is, properties that relate the input and the output of two programs. Our verification method is parametric with respect to the definition of the operational semantics of the programming language in which the two programs are written. That definition of the semantics consists of a set Int of constrained Horn clauses (CHCs) that encode the interpreter of the programming language. Then, given the programs and the relational property we want to verify, we generate, by using Int, a set of constrained Horn clauses whose satisfiability is equivalent to the validity of the property. Unfortunately, state-of-the-art solvers for CHCs have severe limitations in proving the satisfiability, or the unsatisfiability, of such sets of clauses. We propose some transformation techniques that increase the power of CHC solvers when verifying relational properties. We show that these transformations, based on unfold/fold rules, preserve satisfiability. Through an experimental evaluation, we show that in many cases CHC solvers are able to prove the satisfiability (or the unsatisfi- ability) of sets of clauses obtained by applying the transformations we propose, whereas the same solvers are unable to perform those proofs when given as input the original, untransformed sets of CHCs.
23rd International Symposium on Static Analysis, SAS 2016
gbr
2016
23.
Rilevanza internazionale
Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni
English
Intervento a convegno
De Angelis, E., Fioravanti, F., Pettorossi, A., & Proietti, M. (2016). Relational verification through horn clause transformation. In Static analysis: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016: proceedings (pp.147-169). Springer Verlag [10.1007/978-3-662-53413-7_8].
De Angelis, E; Fioravanti, F; Pettorossi, A; Proietti, M
File in questo prodotto:
File Dimensione Formato  
2016_DFPP_SAS.pdf

accesso solo dalla rete interna

Descrizione: Articolo principale
Licenza: Copyright dell'editore
Dimensione 584.1 kB
Formato Adobe PDF
584.1 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: http://hdl.handle.net/2108/184170
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 21
  • ???jsp.display-item.citation.isi??? 19
social impact