ACSAR (Automatic Checker of Safety properties based on Abstraction Refinement)
-
About ACSAR
ACSAR is a model checker for C programs based on the abstraction-refinement paradigm. It can automatically detect runtime errors (array bound violation, buffer overflows, NULL pointer dereferences, etc.). ACSAR checks the validity of a specified assertion for all possible executions. If ACSAR finds that the assertion is potentially violated, it returns a trace (counterexample) representing a scenario of the violation of that assertion.
A specificity of ACSAR is the way it overcomes a problem common to most of the tools based on the abstraction-refinement approach. The problem is the generation of 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 (find more here).
ACSAR was initially developed as part of the Verisoft Project. In that context, ACSAR was used as backend for the the interactive theorem prover Isabelle (see this workwork). More information about the installation and usage of ACSAR are included in the package. -
Download
Linux version of ACSAR_0.1 is available
-
Author
ACSAR is developed by Mohamed Nassim SEGHIR
-
Related Tools