ACSAR: Software Model Checking with Transfinite Refinement

Mohamed Nassim Seghir, Andreas Podelski

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

ACSAR (Automatic Checker of Safety properties based on Abstraction Refinement) is a software model checker for C programs in the spirit of Blast [6], F-Soft [7], Magic [5] and Slam [1]. It is based on the counterexample-guided abstraction refinement (CEGAR) paradigm. Its specificity lies in the way it overcomes a problem common to all tools based on this paradigm. The problem arises from creating more and more spurious counterexamples by unfolding the same (while- or for-) loop over and over again; this leads to an infinite or at least too large sequence of refinement steps. The idea behind ACSAR is to abstract not just states but also the state changes induced by structured program statements, including for- and while-statements. The use of the new abstraction allows one to shortcut such a “transfinite” sequence of refinement steps.
Original languageEnglish
Title of host publicationModel Checking Software
Subtitle of host publication14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings
PublisherSpringer Berlin Heidelberg
Pages274-278
Number of pages5
Volume4595
ISBN (Electronic)978-3-540-73370-6
ISBN (Print)978-3-540-73369-0
DOIs
Publication statusPublished - 2007

Fingerprint

Dive into the research topics of 'ACSAR: Software Model Checking with Transfinite Refinement'. Together they form a unique fingerprint.

Cite this