Software and Benchmarks

[Software] [Benchmark Generators and Instances]

• Smodels - a system for rule-based constraint programming based on logic programs with the stable model semantics implemented in C++
• GnT - a solver for disjunctive logic programs
• circ2dlp - translating parallel circumscriptions into disjunctive logic programs
• (D)LPEQ - software for verifying the equivalence of (disjunctive) logic programs
• lp2sat - translating normal logic programs into propositional theories
• 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
• lbtt - a testbench for implementations of algorithms for translating linear temporal logic (LTL) formulas into Büchi automata.
• 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.