Skip to main content

ExpliSAT

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.

Contact: Dmitry Pidan

Publications

  • S. Barner, C. Eisner, Z. Glazberg, D. Kroening, and I. Rabinovitz, "Explisat: Guiding SAT-based Software Verification with Explicit States," in Proc. of HVC, 2007, pp. 138-154
  • H.Chockler, D.Pidan, and S.Ruah "Improving Representative Computation in ExpliSAT", in Proc. of HVC, 2013, pp. 359-364