Software and Benchmarks
[Benchmark Generators and Instances]
This page contains links to research-related software and benchmarks
developed at the Laboratory for Theoretical Computer Science.
The people and research groups of
the former Laboratory for Theoretical Computer Science joined the
of Information of Computer Science
when it was founded in 2008. So please consider consulting also
the research pages
of the department.
- Smodels - a system for rule-based constraint
programming based on logic programs with the stable model semantics
implemented in C++
- lpeq -
verifying the equivalence of smodels programs / disjunctive logic programs
- lp2diff -
translating normal/smodels programs into difference logic
- lp2sat -
translating normal logic programs into propositional theories
- asptools -
a tool collection for answer set programming
- GnT -
a solver for disjunctive logic programs
- circ2dlp -
translating parallel circumscriptions into disjunctive logic programs
- an implementation of a tableau method for Boolean circuit
satisfiability checking; the description of
the file format for
Boolean circuits and a translator from Boolean circuits to CNF is
- satu -
a SAT solver for computational grids
- MiniUnsat - extracts minimal unsatisfiable subsets (MUSes) from unsatisfiable CNF formulas.
- sateq -
verifying the equivalence of propositional theories in the DIMACS format
- lbtt -
a testbench for implementations of algorithms for translating linear
temporal logic (LTL) formulas into Büchi automata.
- Uppaal_Reader -
a small tool for parsing Uppaal output files to simpler presentation
- For further software developed by the Logic group see the home page
of the group
- Prod - a Pr/T-net reachability analysis tool
with a CTL model checker for the reachability graph and an on-the-fly
LTL model checker using the stubborn set method
- Emma - a TNSDL reachability analysis tool
- Maria - a reachability analyzer for algebraic
system nets (a high-level variant of Petri nets)
- MIPL Mobile IPv6 for Linux -
an implementation of Mobility support in IPv6 Internet Draft
- HUT AODV for IPv6
- an implementation of the Ad hoc On-demand Distance Vector (AODV)
Routing Protocol with IPv6 modifications
- Packet Level Authentication (PLA)
- a proof-of-concept implementation of the Packet Level Authentication protocol -concept
Benchmark Generators and Instances
- genfacbm - a benchmark generator based on
factoring for (Boolean circuit and CNF) SAT and ASP solvers
SAT benchmark generator and instances based on 3-regular graphs
BMC tools translating LTSs to Boolean circuit satisfiability
modeling step and process executions
a tool that constructs Boolean
circuit satisfiability instances from a known plain text attack for DES.
A generator for random NuSMV models.
Also contains scripts
for obtaining random LTL specifications generated by
Spin and Maria models of a distributed system
This page contains
the source codes, benchmarks, and scripts for
the experiments in the paper
"Linear Encodings of Bounded LTL Model Checking"
by Biere, Heljanko, Junttila, Latvala, and Schuppan,
Logical Methods in Computer Science.
Latest update: 08 December 2010.