[  news | formats | fuzzddtools | tools | benchmarks | solvers | bdds | teaching | heuristic-optimization ]

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

News

New SAT Solver Satch used in talks for Simons Institute.

New SAT Competition 2020 release of our SAT solver CaDiCaL.

First release of our new SAT solver Kissat.

New SAT Race 2019 release of our SAT solver CaDiCaL.

First release of our CNF scrambler scranfilize.

New release of our SAT solver Lingeling under MIT style license, which in essence the version submitted to the SAT Competition 2018.

New release of our propositional DRAT proof checker DRABT.

New SAT Solver Splatz

New source code release (version 965) of PicoSAT.

First release of the McRaceTrack model checker.

New source code release (version 2.2.0) of Boolector.

New source code release (version 3.2) of Quantor.

First release of iDQ, an instantiation-based DQBF (Dependency Quantified Boolean Formula) solver for input formules in DQDIMACS format.

First public release of ddsexpr a (classical non-grammar based) fuzzer and delta-debugger for s-expressions.

New release of our CNFuzzDD tool suite.

First release of BV2SMV, a translation tool from QF_BV into SMV.

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.

Software described in our Cube and Conquer paper.

New release of Cleaneling.

First release of QBFcert, a framework for certifying QBF.

New releases of PicoSAT.

New version 1.9.3 of the 1.9 series of AIGER as used in HWMCC'11, HWMCC'12.

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 DepQBF.

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

SAT solver Cleaneling for educational purposes.

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

SAT solver Lingeling with its multi-threaded front end Plingeling.

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.

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

First release of the McRaceTrack model checker.

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.