Software and Benchmarks

[Software] [Benchmark Generators and Instances]

Note: The people and research groups of the former Laboratory for Theoretical Computer Science joined the Department 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
• BCSat - 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 also available.
• 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

• Older software

• 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
• daa and otf - BMC tools translating LTSs to Boolean circuit satisfiability modeling step and process executions
• des2bc - 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 lbtt.
• 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, accepted to Logical Methods in Computer Science.