1 Search Results for "De Angelis, Emanuele"

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-dev.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.}
}
  • Refine by Author
  • 1 De Angelis, Emanuele

  • Refine by Classification

  • Refine by Keyword
  • 1 Software model checking
  • 1 constraint logic programming.
  • 1 program specialization

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2012

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact