Software

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

New version 1.9.3 of the 1.9 series of AIGER used in the upcoming HWMCC'11.

First release of Bloqqer.

Renamed Run to RunLim. There is also a new version.

First release of QxBF.

Resurrected SMVFlatten.

First release of McAiger.

First release of Lingeling and Plingeling.

Source code realease of Boolector.

First release of DepQBF.

New releases of PrecoSAT and PicoSAT.

Formats

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

Fuzzing and Delta-Debugging Tools

We provide fuzzers and delta-debuggers for various kinds of logics.

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

First release of our simple model checker McAiger based on k-induction. It uses symbolic all-different constraints as implemented in PicoSAT.

Our new SAT solver Lingeling with its multi-threaded front end Plingeling was ranked second respectively first in the last SAT Race 2010.

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

Our SAT solver PrecoSAT won three medals in the SAT competition 2009.

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 with an extensive API. It can generate proofs and cores in memory. The proof trace is compressed and thus needs much less space than BooleForce. The most recent version comes with the utility PicoMUS to compute a minimal unsatisfiable core respectively set (MUS).

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 now obsolete SAT solvers: Limmat, Compsat and NanoSAT are available in source. More on the history and the reasoning behind our implementations of these earlier 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.