ExpliSAT is a tool for the formal verification of C/C++ software. Given a program in C/C++, ExpliSAT is verifying that the program satisfies its properties - C assertions embedded within the program itself. Satisfying a property means no feasible execution path can lead to a violation of a corresponding C assertion. ExpliSAT is able either to prove that the property is indeed satisfy, or to falsify it by providing a counter example - C test case leading to an assertion violation.

ExpliSAT verifies a program using symbolic interpretation - combining explicit exploration of every feasible execution path of the program with symbolic representation of input variables. Symbolic representation of an input variable has a semantics of "a variable can take any value in its domain". Thus, by evaluating a single execution path, ExpliSAT actually verifies absence of failures for every possible input of a program that leads it through this execution path.

Currently, ExpliSAT is used in embedded software projects, for unit testing of critical pieces of code.



Dmitry Pidan, Emerging Security & Quality Technologies, IBM Research - Haifa