ExpliSAT (PINCETTE)     


Ronen Levy photo

ExpliSAT (PINCETTE) - overview

ExpliSAT is a software model-checking tool for C and C++ based on a hybrid methodology of explicit control flow traversal and symbolic data representation - what can be called "concolic model checking". This approach combines the merits of SAT-based symbolic model checking and explicit-state model checking, while avoiding the state-explosion problem. The later is because the SAT solver is invoked for each control flow path separately, rather than for the whole program. Moreover, ExpliSAT uses explicit values in order to guide the search towards legal program paths only. ExpliSAT is able to verify implicit and user-defined assertions in programs, where implicit assertions are ones that should hold in all programs, such as "no null pointer dereference", and user-defined ones describe the desired functionality of the program.