Software

• ASPTOOLS: a tool collection for answer-set programming.
• SATTOOLS: a tool collection for Boolean satisfiability.
• SSOKOBAN: an smodels/perl program that solves sokoban levels (including a patch for xsokoban).
• MCSMODELS a deadlock and reachability checker which uses finite complete prefixes generated by the PEP tool from 1-safe Petri nets and employes smodels as its computational engine.
• PUNROLL: a bounded reachability checker based on process semantics.
• BOUNDSMODELS: a bounded model checker for LTL.
• UNFSMODELS: an LTL model checker using net unfoldings.
• BOMOTEST: a testing tool.
• BCSAT: 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.
• GENFACBM: a benchmark generator based on factoring for SAT and ASP solvers.
• LBTT: a testbench for implementations of algorithms for translating linear temporal logic (LTL) formulas into Büchi automata.