ACSAR (Automatic Checker of Safety properties based on Abstraction Refinement)
Introduction
ACSAR is a model checker for C programs based on the abstraction-verification-refinement paradigm. It is used for the automatic detection of runtime errors (array out of bounds, buffer overflow, NULL pointer dereference, etc.). Using ACSAR, one can specify that an assertion will never be violated. While in the context of programming languages an assertion is checked for the current execution of the program, ACSAR checks the validity of the assertion for all possible executions. If ACSAR finds that the specified assertion can be violated, it returns a trace (counter example) that represents a scenario of execution leading to the violation of that assertion.
A specificity of ACSAR is the way it overcomes a problem common to all tools based on the abstraction-refinement approach. 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.
ACSAR is developed as part of the Verisoft Project.
More information about
the installation and the usage are included in the package.
Download
Linux version of ACSAR_0.1 is available
Author
ACSAR is developed by Mohamed Nassim SEGHIR
Related Tools