LIPIcs.ICLP.2012.439.pdf
- Filesize: 355 kB
- 6 pages
Document
Software Model Checking by Program Specialization
Author
-
Part of:
Volume:
Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (ICLP 2012)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Logic Programming (ICLP) - License:
Creative Commons Attribution-NoDerivs 3.0 Unported license
- Publication Date: 2012-09-05
Cite AsGet BibTex
Emanuele De Angelis. Software Model Checking by Program Specialization. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 439-444, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/LIPIcs.ICLP.2012.439
https://doi.org/10.4230/LIPIcs.ICLP.2012.439
Abstract
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 phi in a logic M, we can verify that phi 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 phi, 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.
Keywords
- Software model checking
- program specialization
- constraint logic programming.
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads