Bibliograph.
Daten | Kiefer, Stefan: Abstraction Refinement for Pushdown Systems.
Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, Diplomarbeit Nr. 2284 (2005).
81 Seiten, englisch.
|
|---|
| CR-Klassif. | D.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
|
|---|
| Keywords | verification; model checking; pushdown systems; abstraction refinement; Craig interpolation |
|---|
| Kurzfassung | 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.
|
|---|
Volltext und
andere Links | PDF (570688 Bytes)
PostScript (912391 Bytes)
Zugriff auf studentische Arbeiten aufgrund vorherrschender Datenschutzbestimmungen nur innerhalb der Fakultät möglich |
|---|
| Kontakt | kiefersn@fmi.uni-stuttgart.de |
|---|
| Abteilung(en) | Universität Stuttgart, Institut für Formale Methoden der Informatik, Sichere und Zuverlässige Softwaresysteme
|
|---|
| Eingabedatum | 24. Mai 2005 |
|---|