Software

On this page you find a partial list of software provided by FMV.

First release of DepQBF.

Second release of PrecoSAT.

Formats

Based on And-Inverter Graphs (AIGs) we developed a format AIGER to describe structural SAT and model checking benchmarks.

Answer Set Programming (ASP) Tools

FuzzASP is a fuzzer that can be used to generate random answer set programs.

DeltaASP is a delta-debugger which is able to to automatically minimize failure-inducing answer set programs in the syntax of lparse.

Satisfiability Modulo Theories (SMT) Tools

FuzzSMTBV is a light-weight fuzzer that can be used to generate random SMT benchmarks with bit-vectors and arrays.

FuzzSMT is a more sophisticated SMT fuzzer that supports almost all relevant logics of the SMT-LIB.

DeltaSMT is a delta-debugger which is able to to automatically minimize failure-inducing SMT benchmarks. It can be particularly useful in the process of debugging SMT solvers.

VoteSMT is a parallel majority voting framework for SMT solvers. It can be used to find and classify failure-inducing SMT benchmarks.

Miscellaneous Tools

The converter cnf2aig extracts AIGs in AIGER format from a CNF in DIMACS format.

The tool run can be used for sampling time and memory usage of programs.

Benchmarks

With our tool smv2qbf we generated some QBF benchmarks.

Simple model checking benchmarks in AIGER format.

Solvers

DepQBF is a search-based QBF solver which tries to exploit independence between variables.

Our new SAT solver PrecoSAT won three medals in the last SAT competition.

Boolector is an SMT solver for the theory of bit-vectors and the extensional theory of arrays over bit-vectors. It won first places in the prestigious bit-vector and bit-vector with arrays tracks in the SMT competition 2008. In the latest SMT competition, it won the second place in the bit-vector division and again the first place in the division of bit-vectors and arrays.

PicoSAT is a SAT solver turned out to be faster on industrial instances than MiniSAT 2.0 and also can generate proofs and cores in memory. The proof trace is compressed and thus needs much less space than BooleForce.

BooleForce is a SAT solver similar to MiniSAT which can generate proofs and cores in memory.

C32SAT is a satisfiability checker for boolean C expressions. It can check whether they can be satisfied, are tautological, or can potentially be undefined according to the C99 standard.

Quantor is a solver for quantified boolean formulas (QBF). We have also implemented various SAT solvers. Limmat, Compsat and NanoSAT are available in source.

More on the history and the reasoning behind our implementations of our SAT solvers can be found in our technical report "The Evolution from Limmat to Nanosat".

The source code of our BDD based SAT solver EBDDRES is available.

We provide a trace checker for propositional resolution proofs.

BDDs

Before SAT and QBF we worked on model checking with binary decision diagrams (BDDs). Our BDD based model checker Mucke comes with two BDD libraries, one of them, ABCD, can be obtained separately.

Teaching

The finite state machine calculator FSMCalc implements data structures and algorithms of Formal Models (FG3) and Model Checking (Systemtheory 1).

You may also want to check out our CNF encoder Limboole. It has a more user friendly input format than CNF and is a perfect supplement for an introductory course in logic.

We implemented an elevator simulation elsim. It can be used for illustrating the concepts of safety, liveness and quantitative temporal properties.

There is also a train collision example zug.

Heuristic Optimization

The HeuristicLab is a paradigm-independent, flexible, extensible, and comfortable environment for heuristic optimization. It is implemented in C# within the Microsoft .NET framework.