5 Tools

The following is a partial list of state-of-the-art tools that implement the techniques covered in the course. It is designed to serve as inspiration for the kinds of tools you may want to use or build in the course project. Some of them will also be featured in the homework assignments.

5.1 SAT solving

• Glucose (great at solving hard instances)

• Lingeling, Plingeling and Treengeling (won 4 tracks of the SAT’14 competition)

• CryptoMiniSAT (supports XOR constraints)

• MiniSAT (a classic, minimalistic SAT solver)

• SAT4J (also solves MAXSAT, Pseudo-Boolean, and Minimal Unsat Core problems)

5.2 SMT solving

• Z3 (supports many theories, best in 16 tracks of SMT-COMP’14)

• CVC4 (supports many theories, won 14 tracks of SMT-COMP’14)

• Yices (supports many theories, won 10 tracks of SMT-COMP’14)

• Boolector (supports bitvectors and arrays, won the ABV track of SMT-COMP’14)

5.3 Finite Model Finding

• Kodkod and Alloy (relational logic)

• Nitrox (higher-order logic)

• IDP (first-order logic with inductive definitions)

• MACE4 (first-order logic)

5.4 Verification

• Dafny (an imperative and functional programming language with a verifier)

• Boogie (an intermediate verification language—great for building other tools)

• VCC (a verifier for concurrent C programs)

• Leon (a verifier and synthesizer for Scala)

5.5 Bounded Verification

• CBMC (a bounded model checker for C)

• TACO (a bounded verifier for Java)

• Rubicon (a bounded verifier for Ruby)

5.6 Symbolic Execution

• Klee (a symbolic execution engine for C)

• Java Path Finder (JPF) (a symbolic execution engine for Java)

5.7 Model Checking

• SPIN (an explicit state model checker)

• Murphi (an explicit state model checker)

• NuSMV (a symbolic model checker)

5.8 Synthesis, Declarative Execution, and Fault Localization

• SKETCH (an imperative language with a synthesizer)

• Kaplan (declarative execution for Scala)

• Squander and PBnJ (declarative execution for Java)

• BugAssist (fault localization for C)