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.

SAT solving

• Glucose (great at solving hard instances)
• Lingeling (won 4 tracks of the SAT’14 competition)
• CryptoMiniSAT (supports XOR constraints; won the incremental track of the SAT-Race 2015)
• MiniSAT (a classic, minimalistic SAT solver)
• SAT4J (also solves MAXSAT, Pseudo-Boolean, and Minimal Unsat Core problems)

SMT solving

• Z3 (supports many theories, won 24 tracks of SMT-COMP’15)
• CVC4 (supports many theories, won 12 tracks of SMT-COMP’15)
• Yices (supports many theories, won 10 tracks of SMT-COMP’15)
• Boolector (supports bitvectors and arrays, won 3 tracks of SMT-COMP’15)

Finite model finding

• Kodkod and Alloy (relational logic)
• Nitrox (higher-order logic)
• IDP (first-order logic with inductive definitions)
• MACE4 (first-order logic)

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)

Bounded verification

• CBMC (a bounded model checker for C)
• Rubicon (a bounded verifier for Ruby)
• TACO (a bounded verifier for Java)

Symbolic execution

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

Synthesis and more

• SKETCH (an imperative language for synthesis)
• Rosette (a solver-aided host language)
• Kaplan (declarative execution for Scala)
• Squander (declarative execution for Java)
• BugAssist (fault localization for C)