swMATH ID: 2684
Software Authors: Seghir, M.N., Podelski, A.
Description: 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.
Homepage: http://link.springer.com/chapter/10.1007/978-3-540-73370-6_19
Keywords: synthetic aperture radar imaging
Related Software: SLAM; SatAbs; SIMPLIFY; PVS; ARMC
Cited in: 3 Publications

Cited in 0 Serials

Citations by Year