ACSAR: Software model checking with transfinite refinement. 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.

References in zbMATH (referenced in 4 articles )

Showing results 1 to 4 of 4.
Sorted by year (citations)

  1. Seghir, Mohamed Nassim: An assume guarantee approach for checking quantified array assertions (2011)
  2. Seghir, Mohamed Nassim: A lightweight approach for loop summarization (2011)
  3. Seghir, Mohamed Nassim; Podelski, Andreas; Wies, Thomas: Abstraction refinement for quantified array assertions (2009)
  4. Nassim Seghir, Mohamed; Podelski, Andreas: ACSAR: Software model checking with transfinite refinement (2007) ioport