IBM Software Formal Verification Tool (ExpliSAT)       


 Karen Yorav photo

IBM Software Formal Verification Tool (ExpliSAT) - overview

ExpliSAT is a tool for the verification of C/C++ software. Given a program in C/C++, ExpliSAT verifies that the program satisfies a wide set of correctness properites as well as embedded assertions. By default, ExpliSAT will verify that the code satisfies various memory safety properties, pointer safety properties, arithmetic properties and more. In addition, any C-assertions that are embedded into the code will also be verified.

Verifying a property means checking that no feasible execution path can lead to a violation of the corresponding C assertion or built-in check. ExpliSAT will either prove that the property is indeed satisfied, or will show that it is not satisfied by producing a counterexample - a C test case leading to a violation. This test case can be compiled together with the program code and examined using a debugger.

ExpliSAT is based on symbolic interpretation - combining an explicit exploration of every feasible execution path of the program with a symbolic representation of input values. Symbols are injected instead of input values, where a symbol represents any value in the corresponding domain. Thus, the evaluation of an execution path verifies the absence of failures on all possible inputs that lead the program through this execution path.

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