Semantics-based generation of verification conditions by program specialization
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti · 2015
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.