Research : Projects

STORM

STORM is a tool for detection of concurrency errors in system software written in C. More information and source code are available on STORM’s webpage (still under construction).

SMACK

SMACK (Static Modular Assertion ChecKer) is a tool for checking properties of system software written in C. It is similar in spirit to HAVOC. However, as opposed to HAVOC which is based on Microsoft’s proprietary infrastructure, SMACK is open-source and uses the open-source LLVM compiler infrastructure. Therefore, SMACK can check a different spectrum of programs: a large number of gcc-based, mainly open-source applications that are readily available. It should also be relatively easy to implement and try out different extensions on top of SMACK.

SMACK is hosted on GitHub: http://smackers.github.io/smack

HAVOC

During my first internship at Microsoft Research back in 2006, I was involved in creating the foundations of HAVOC. HAVOC is a verifier for C programs built on top of Microsoft’s Visual C compiler (cl.exe), and therefore is targeting Windows programs. It transforms a C program into a BoogiePL program, which is the input of the well-known Boogie verification-condition (VC) generator. Generated VCs are handed over to the Z3 theorem prover. Based on the VC’s validity, the verification either succeeds or the tool returns an error trace.

STRACLOS

STRACLOS is a fast decision procedure for our Simple TRAnsitive CLOSure logic. The logic is suitable for reasoning about linked data structures, and contains convenient constructs for expressing unbounded reachability in such structures. Therefore, it can be used for verification of heap-manipulating programs that operate on linked lists. We successfully used STRACLOS to verify a number of heap-manipulating programs using predicate abstraction. Source code and Linux binary distribution are available for download:

STRACLOS has also been integrated into an available SMT solver MathSAT (big thanks to Roberto Bruttomesso and Alessandro Cimatti for helping out!). The version of MathSAT extended with STRACLOS (i.e. the theory of unbounded reachability) can be downloaded from the MathSAT homepage. Here are benchmarks from this work:

STRACLOS is joint work with Jesse Bingham.

Comments are closed.