Software: FMSD'12 version of CHIMP (CHIMP Handles Instrumentation for Monitoring of Properties)
Author(s): Deian Tabakov, Kristin Y. Rozier
Comments: 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
Documentation: available in the package
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
Documentation: available in the package
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 (See comments)
Comments: Multi-resolution with ZDDs implementation copyright Laurent Simon (homepage) used under permission.  Graph Library copyright Andrew Ladd (homepage) 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.