| Software | TraceSampler |
| Author(s) | Aditya Shrotri |
| Description | A suite of algorithms for uniformly sampling traces of a transition system. |
| Software | Matrix Permanent |
| Author(s) | Aditya Shrotri |
| Description | A suite of algorithms for computing the permanent of a matrix. |
| Software | DNF Counting |
| Author(s) | Aditya Shrotri |
| Description | A suite of algorithms for counting DNF formulas. |
| Software | DPMC |
| Author(s) | Jeffrey Dudek, Vu Phan |
| Description | An exact weighted model-counting framework based on algebraic decision diagrams and tensors. |
| Software | RSynth |
| Author(s) | Lucas Tabajara |
| Description | A BDD-based Boolean-synthesis tool. |
| Software | FourierSAT |
| Author(s) | Zhiwei Zhang |
| Description | A continuous local search SAT solver based on Fourier expansion for hybrid Boolean constraints. |
| Software | TensorOrder |
| Author(s) | Jeffrey Dudek |
| Description | A tool for weighted model counting through tensor network contraction. |
| Software | ADDMC |
| Author(s) | Vu Phan |
| Description | An exact weighted model counter based on algebraic decision diagrams. |
| Software | Corpus |
| Author(s) | Corey Fisher |
| Description | Haskell source code for generating random automata. |
| Software | Rank |
| Author(s) | Seth Fogarty, extending the Mh program by Laurent Doyen and J.F. Raskin |
| Description | Buchi containment solver, employing the antichain-based algorithm in Doyen, L., Raskin, J.-F., Antichains for the automata-based approach to model-checking. LMCS 1(5) 2009 |
| Software | Ramsey |
| Author(s) | Seth Fogarty, extending the sct/scp program by Amir Ben-Amram and Chin Soon Lee. |
| Description | Buchi containment solver, employing the Ramsey-based algorithm with subsumption in FV2010. |
| Software | WeightGen |
| Author(s) | Kuldeep S. Meel |
| Description | Please see the WeightGen project page for more detail. |
| Software | WeightMC |
| Author(s) | Kuldeep S. Meel |
| Software | UniGen |
| Author(s) | Kuldeep S. Meel |
| Software | ApproxMC |
| Author(s) | Kuldeep S. Meel |
| Software | FMSD'12 version of CHIMP (CHIMP Handles Instrumentation for Monitoring of Properties) |
| Author(s) | Deian Tabakov, Kristin Y. Rozier |
| Description | This version of CHIMP implements the table-based encodings described in our FMSD'12 paper. It was upgraded to work with SPOT v0.8. |
| Software | CHIMP (CHIMP Handles Instrumentation for Monitoring of Properties) |
| Author(s) | Deian Tabakov |
| Comments | Implementation of the LTL-to-monitor approach described by the Ph.D. thesis of the tool author. This tool uses SPOT 0.4 to generate Büchi automata that accept all traces of the provided LTL formulas. The Büchi automata are then converted to nondeterministic finite-word automata that accept all illegal executions (see the Ph.D. thesis for further details). The tool may apply minimization of the automaton using the BRICS Automaton tool (see below for related code). After all optimizations and transformations have been performed, the tool generates a C/C++ monitor that detects all illegal executions ("bad prefixes"). Extract the bzip-ed tar-ed archive using tar -xvjf monitor_master.tar.bz2. You can see a sample monitor file, corresponding to the property G p. |
| Description | The tool uses SPOT for the LTL-to-Büchi conversion; substituting another converter is possible if the user uses a different language for specifying the properties of the system, e.g., PSL or SVA. This code supports SPOT v.0.4; in case future versions of SPOT are incompatible with the code, you can download the version that the author used (spot-0.4.tar.bz2). The source code already #includes the required SPOT header files, so you have to provide the path to SPOT's installation when compiling, and you have to link to SPOT's libspot.a and libbdd.a to produce the final assembly. |
| Software | automaton-1.11_addon.tar.bz2 |
| Author(s) | Deian Tabakov |
| Comments | The monitor generation tool, monitor master, has an optional automaton minimization flag. When the flag is set, the tool exports the automaton using the LBT format and then uses a shell command to minimize it using the BRICS Automaton tool. Since BRICS Automaton does not parse natively automata in LBT format, we need an add-on to parse the automaton, use BRICS Automaton to determinize and minimize it, and then convert the minimized automaton back to LBT format. The required code is provided here as Java source code. |
| Description | Extract the bzip-ed tar-ed archive using tar -xvjf automaton-1.11_addon.tar.bz2 in the top directory of BRICS Automaton. The new code is in src/dk/brics/extra/. This code worked with version 1.11 of BRICS Automaton. In case it does not work with future versions of BRICS Automaton, you can try downloading version 1.11 with the add-on in one package as automaton-1.11_plus_addon.tar.bz2. You can override the default location where monitor master is looking for the BRICS Automaton code by editing the monitor master file global_params.cc and changing the definition of brics_root inside the constructor to point to the root of the BRICS Automaton source. This can also be done on the command line by providing the switch -brics_root /path/to/brics_automaton/root. |
| Software | adders.tar.bz2 and airline.tar.bz2 |
| Author(s) | Deian Tabakov |
| Comments | SystemC models used in the Ph.D. thesis of the tool author. |
| Description | These SystemC models are self-contained and should work with SystemC-2.2.0 or later. They can also be run using the modified SystemC kernel (see the author's Ph.D. thesis for details) and verified using runtime verification. |
| Software | systemc-2.2.0_patch.tar.bz2 |
| Author(s) | Deian Tabakov |
| Comments | A patch to update SystemC-2.2.0 with runtime verification support, as discussed in the Ph.D. thesis of the patch author. |
| Description | See README in the archive. |
| Software | systemc-2.2.0_with_RV_support.tar.bz2 |
| Author(s) | Deian Tabakov |
| Comments | Full source code of the modified version of SystemC-2.2.0 as described in the Ph.D. thesis of the tool author. |
| Description | Full source code in case applying the patch does not work, or in case version 2.2.0 is no longer available for download. |
| Software | LTL2AUT |
| Author(s) | Marco Daniele |
| Description | LTL2AUT generates Buchi automata from LTL formulas. The software is also described in the CAV 1999 paper by Marco Daniele, Fausto Giunchiglia, and Moshe Y. Vardi. |
| Software | KBDD |
| Author(s) | Guoqiang Pan |
| Description | BDD-based satisfiability solver for modal logic K. The software is also described in the CADE 2002 paper by Guoqiang Pan, Ulrike Sattler, and Moshe Y. Vardi and the CADE 2003 paper by Guoqiang Pan and Moshe Y. Vardi. |
| Software | QMRes |
| Author(s) | Guoqiang Pan |
| Comments | Multi-resolution with ZDDs implementation copyright Laurent Simon used under permission. Graph Library copyright Andrew Ladd used under permission download here (this version is modified to include vertex ordering heuristics). Download binary only for QMRes here. |
| Description | ZDD-based multi-resolution solver for QBF. The software is also described in the CP 2004 paper by Guoqiang Pan and Moshe Y. Vardi. |