Diploma Thesis DIP-2284

BibliographyKiefer, Stefan: Abstraction Refinement for Pushdown Systems.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Diploma Thesis No. 2284 (2005).
81 pages, english.
CR-SchemaD.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
Keywordsverification; model checking; pushdown systems; abstraction refinement; Craig interpolation
Abstract

This thesis adapts the paradigm of CEGAR (counterexample-guided abstraction refinement) to the model checking of pushdown systems.

A theoretical framework based on Craig interpolation is developed and applied to the automatic abstraction of sequential programs. It is generalized to handle full pushdown systems, including recursion, as well as multiple counterexamples.

It is shown that this theory provides a framework for different heuristics to compute relevant predicates. Several concrete heuristics are proposed and discussed.

An implementation based on the model checker Moped gives evidence of the usefulness of the developed concepts. In contrast to other approaches, Binary Decision Diagrams (BDDs) are used throughout the CEGAR loop.

Full text and
other links
PDF (570688 Bytes)
PostScript (912391 Bytes)
Access to students' publications restricted to the faculty due to current privacy regulations
Contactkiefersn@fmi.uni-stuttgart.de
Department(s)University of Stuttgart, Institute of Formal Methods in Computer Science, Software Reliability and Security
Entry dateMay 24, 2005
   Publ. Computer Science