DROPS

Document

DOI: 10.4230/LIPIcs.ICLP.2012.439

Software Model Checking by Program Specialization

Authors: Emanuele De Angelis

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

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

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)

Copy BibTex To Clipboard

@InProceedings{deangelis:LIPIcs.ICLP.2012.439,
  author =	{De Angelis, Emanuele},
  title =	{{Software Model Checking by Program Specialization}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{439--444},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.439},
  URN =		{urn:nbn:de:0030-drops-36436},
  doi =		{10.4230/LIPIcs.ICLP.2012.439},
  annote =	{Keywords: Software model checking, program specialization, constraint logic programming.}
}

Search Results

Documents authored by De Angelis, Emanuele

Software Model Checking by Program Specialization

Abstract

Cite as

Thanks for your feedback!

Could not send message