On this page you find a partial list of software provided by FMV.
First release of BV2EPR, a translation tool from QF_BV into EPR.
First release of ddSMT, a delta debugger for SMT-LIB v2 benchmarks.
First source code release of JNuke. A program analysis framework for Java.
New release source code release of Boolector.
New release of Lingeling (includes Plingeling, Blimc, iLingeling).
New release of Cleaneling.
First release of QBFcert, a framework for certifying QBF.
New releases of PicoSAT.
First release of Bloqqer.
First release of QxBF.
First release of McAiger.
First release of DepQBF.
Based on And-Inverter Graphs (AIGs) we developed a format AIGER to describe structural SAT and model checking benchmarks.
We provide fuzzers and delta-debuggers for various kinds of logics.
The tool run can be used for sampling time and memory usage of programs.
SAT solver Cleaneling for educational purposes.
DepQBF is a search-based QBF solver which tries to exploit independence between variables.
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.
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.
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.
The HeuristicLab is a paradigm-independent, flexible, extensible, and comfortable environment for heuristic optimization. It is implemented in C# within the Microsoft .NET framework.