Software Model Checking by Program Specialization

Author Emanuele De Angelis

Thumbnail PDF


  • Filesize: 355 kB
  • 6 pages

Document Identifiers

Author Details

Emanuele De Angelis

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)


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.
  • Software model checking
  • program specialization
  • constraint logic programming.


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads