This is a collection of tools that you can explore for your semester project. Homework assignments will also make use of some of these tools.
The tools fall into the following categories: Sat Solvers | SMT Solvers | Finite Model Finding | Verification | Bounded Verification | Symbolic Execution | Model Checking | Synthesis, Declarative Execution and Fault Localization | Solver-Aided Languages
| Tool | Notes |
|---|---|
| Glucose | Glucose is great at solving hard instances. It is designed to be parallel, since 2014. The name of the Solver name is a contraction of the concept of "glue clauses", a particular kind of clauses that glucose detects and preserves during search. |
| Lingeling, Plingeling and Treengeling | Lingeling and its parallel versions Plingeling and Treengeling, obtained first places in 4 tracks (out of 11) of the SAT'14 Competition and thus won 4 Gödel medals during the FLoC'14 Olympic Games. Lingeling also won a first place in the Configurable SAT Solver Challenge (CSSC'14). |
| CryptoMiniSat | CryptoMiniSat supports XOR constraints. The system has 3 interfaces: command-line, C++ library and python. |
| MiniSat | A classic SAT solver. The solver is known for its ability to maintain a small code base, without general loss of perfance compared to other modern SAT solvers. The first version was just above 600 lines, not counting comments and empty lines. |
| Sat4j | Sat4j is a java library for solving boolean satisfaction and optimization problems. It can solve SAT, MAXSAT, Pseudo-Boolean, and Minimally Unsatisfiable Subset (MUS) problems. |
| Z3 | Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types. |
| CVC4 | CVC4 is an efficient open-source automatic theorem prover for SMT problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. |
| Yices | Yices 2 is an SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, real and integer arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both linear and nonlinear arithmetic. |
| Boolector | A SMT solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Boolector won first place in divisions QF_ABV (main, application track), QF_BV (main track) and QF_UFBV (main, application track) in the SMT competition 2018. |
| Kodkod | Kodkod is an efficient SAT-based constraint solver for first order logic with relations, transitive closure, bit-vector arithmetic, and partial models. It provides automated reasoning facilities for both satisfiable and unsatisfiable problems. |
| Alloy | Alloy is an open source language for software modeling. Alloy’s tool, the Alloy Analyzer, is a solver that takes the constraints of a model and finds structures that satisfy them. It can be used both to explore the model by generating sample structures, and to check properties of the model by generating counterexamples. |
| IDP | IDP is a knowledge Base System (KB-system) for the FO(·) language. FO(·) is an extension of first-order logic (FO) with types, aggregates, inductive definitions, bounded arithmetic, partial functions, etc |
| MACE4 | Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. If satisfiability is detected, one or more models are printed. |
| Dafny | Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. |
| Boogie | Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Dafny and VCC use Boogie. |
| IDP | VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program actually meets its specifications. |
| MACE4 | Leon is an automated system for verifying, repairing, and synthesizing functional Scala programs. |
| CBMC | CBMC is a Bounded Model Checker for C and C++ programs. CBMC verifies memory safety, checks for exceptions, checks for various variants of undefined behavior, and user-specified assertions. |
| FORGE | Forge is a program analysis framework that allows a procedure in a conventional object oriented language to be automatically checked against a rich interface specification. |
| Rubicon | Rubicon is a library for Ruby, Rails, and RSpec that lets you write formal specifications of the behavior of your web apps. Rubicon gives you the quantifiers of first-order logic, so your specifications cover all possible objects of the given type. |
| KLEE | KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure, and available under the UIUC open source license. |
| JPF | Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. |
| SPIN | SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion. |
| Murphi | Murphiis an enumerative (explicit state) model checker, with its own input language (also called Murphi) which is a guard -> action notation similar to Unity, which are repeatedely executed in an infinite loop. |
| NuSMV | NuSMV is new symbolic model checker. NuSMV is a reimplementation and extension of SMV, the first model checker based on BDDs. |
| Sketch | SKETCH is a software synthesis tool that allows for rapid development of highly tuned bug-free algorithm implementations. To do this, the programmer develops a sketch, or partial implementation, and a separate specification of the desired functionality. The synthesizer then completes the sketch to behave like the specification. |
| KAPLAN | Kaplan is an extension of the Scala programming language that supports constraint-solving. |
| Squander | Squander is a framework that provides a unified environment for writing declarative constraints and imperative statements in the context of a single program. By being able to mix imperative code with executable declarative specifications, the user can easily express constraint problems in-place. |
| PBnJ | Plan B, performs dynamic contract checking of methods. Plan B as well as its instantiation in an extension to Java with executable specifications forms the tool PBnJ. |
| Bug-Assist | Bug-Assist takes as input an ANSI-C program annotated with assertions, performs model checking internally to find potential assertion violations, and for each error trace returned by the model checker, returns a small number of lines of code which can be changed to eliminate the error trace. |
| Rosette | To verify or synthesize code, Rosette compiles it to logical constraints solved with off-the-shelf SMT solvers. By combining virtualized access to solvers with Racket’s metaprogramming, Rosette makes it easy to develop synthesis and verification tools for new languages. |
| Racket | Racket is a general-purpose programming language as well as the world’s first ecosystem for language-oriented programming. |