Software Model Checking by Program Specialization

De Angelis, Emanuele

doi:10.4230/LIPIcs.ICLP.2012.439

Document

Software Model Checking by Program Specialization

Author Emanuele De Angelis

Part of: Volume: Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (ICLP 2012)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Logic Programming (ICLP)
License: Creative Commons Attribution-NoDerivs 3.0 Unported license
Publication Date: 2012-09-05

PDF

File

PDF

LIPIcs.ICLP.2012.439.pdf

Filesize: 355 kB
6 pages

Document Identifiers

DOI: 10.4230/LIPIcs.ICLP.2012.439
URN: urn:nbn:de:0030-drops-36436

Subject Classification

Keywords

Software model checking
program specialization
constraint logic programming.

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get 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

Author Details

Emanuele De Angelis

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail