Technischer Bericht TR-2006-02

Bibliograph.
Daten
Esparza, Javier; Kiefer, Stefan; Schwoon, Stefan: Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems.
Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, Technischer Bericht Informatik Nr. 2006/02.
21 Seiten, englisch.
CR-Klassif.D.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
Keywordscounterexample-guided abstraction refinement; pushdown systems; Craig interpolation
Kurzfassung

Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this paper, we investigate this concept in the context of sequential (possibly recursive) programs whose statements are given as BDDs. We examine how Craig interpolants can be computed efficiently in this case and propose a new, special type of interpolants. Moreover, we show how to treat multiple counterexamples in one refinement cycle. We have implemented this approach within the model-checker Moped and report on experiments.

Volltext und
andere Links
PDF (224548 Bytes)
PostScript (517293 Bytes)
Abteilung(en)Universität Stuttgart, Institut für Formale Methoden der Informatik, Sichere und Zuverlässige Softwaresysteme
Eingabedatum23. Januar 2006
   Publ. Institut   Publ. Informatik