a tool collection for answer-set programming.
a tool collection for Boolean satisfiability.
an smodels/perl program that solves sokoban levels
(including a patch for
a deadlock and reachability checker which
uses finite complete prefixes generated by the
from 1-safe Petri nets and employes smodels as its computational engine.
a bounded reachability checker based on process semantics.
a bounded model checker for LTL.
an LTL model checker using net unfoldings.
a testing tool.
an implementation of a tableau method for Boolean circuit
satisfiability checking. The file format for Boolean circuits and a
translator from Boolean circuits to CNF is also available.
a benchmark generator based on factoring for SAT and ASP solvers.
a testbench for implementations of algorithms for translating linear
temporal logic (LTL) formulas into Büchi automata.