ACSAR 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 by 3 Authors 3 Seghir, Mohamed Nassim 1 Podelski, Andreas 1 Wies, Thomas Cited in 0 Serials Cited in 1 Field 3 Computer science (68-XX) Citations by Year