Software model checking by program specialization. (English) Zbl 1281.68077

Dovier, Agostino (ed.) et al., Technical communications of the 28th international conference on logic programming (ICLP 2012), September 4–8, 2012, Budapest, Hungary. Papers based on the presentations at the conference. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-43-9). LIPIcs – Leibniz International Proceedings in Informatics 17, 439-444, electronic only (2012).
Summary: We introduce a general verification framework based on program specialization to prove properties of the runtime behaviour of imperative programs. Given a program \(P\) written in a programming language \(L\) and a property \(\varphi\) in a logic \(M\), we can verify that \(\varphi\) holds for \(P\) by: (i) writing an interpreter \(I\) for \(L\) and a semantics \(S\) for \(M\) in a suitable metalanguage, (ii) specializing \(I\) and \(S\) with respect to \(P\) and \(\varphi\), and (iii) analysing the specialized program by performing a further specialization. We have instantiated our framework to verify safety properties of a simple imperative language, called SIMP, extended with a nondeterministic choice operator. The method is fully automatic and it has been implemented using the MAP transformation system.
For the entire collection see [Zbl 1253.68010].


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N17 Logic programming


Full Text: DOI