We present a method for automatically generating verification conditions for a class of imperative programs and safety properties. Our method is parametric with respect to the semantics of the imperative programming language, as it specializes, by using unfold/fold transformation rules, a Horn clause interpreter that encodes that semantics. We define a multi-step operational semantics for a fragment of the C language and compare the verification conditions obtained by using this semantics with those obtained by using a more traditional small-step semantics. The flexibility of the approach is further demonstrated by showing that it is possible to easily take into account alternative operational semantics definitions for modeling new language features. Finally, we provide an experimental evaluation of the method by generating verification conditions using the multi-step and the small-step semantics for a few hundreds of programs taken from various publicly available benchmarks, and by checking the satisfiability of these verification conditions by using state-of-the-art Horn clause solvers. These experiments show that automated verification of programs from a formal definition of the operational semantics is indeed feasible in practice.
De Angelis, E., Fioravanti, F., Pettorossi, A., & Proietti, M. (2015). Semantics-based generation of verification conditions by program specialization. In Proceedings of the 17th International Symposium on principles and practice of declarative programming, PPDP 2015 (pp.91-102). Association for Computing Machinery [10.1145/2790449.2790529].
|Autori:||De Angelis, E; Fioravanti, F; Pettorossi, A; Proietti, M|
|Titolo:||Semantics-based generation of verification conditions by program specialization|
|Nome del convegno:||17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015|
|Luogo del convegno:||Siena, Italy|
|Anno del convegno:||2015|
|Numero del convegno:||17.|
|Data di pubblicazione:||2015|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1145/2790449.2790529|
|Settore Scientifico Disciplinare:||Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni|
|Tipologia:||Intervento a convegno|
|Citazione:||De Angelis, E., Fioravanti, F., Pettorossi, A., & Proietti, M. (2015). Semantics-based generation of verification conditions by program specialization. In Proceedings of the 17th International Symposium on principles and practice of declarative programming, PPDP 2015 (pp.91-102). Association for Computing Machinery [10.1145/2790449.2790529].|
|Appare nelle tipologie:||02 - Intervento a convegno|