Software Tools
Asterix
A theorem prover for separation logic entailments presented at APLAS 2013. Utilises a model-based approach that leverages SMT proving to reason about heap properties. It won the SL-COMP theorem-proving competition in the categories with acyclic list segments in 2014, 2018, and 2019. The binaries provided here are known to run on Ubuntu 14.04 LTS 64-bit.
- asterix-ubuntu.zip (7.8 MB, 17 Jun 2014)
Cardan
Linux/x86 binaries of the Cardan tool to translate declarative rules of a P2 program into a transition relation suitable for analysis with the ARMC model checker. An updated binary of ARMC is also included. It is based on an abstraction approach described at CAV 2009.
- cardan.tar.gz (2.3 MB, 29 Jan 2009)
Spinn3r
Scripts to extract data from the Spinn3er blog dataset. They gather data about all the posts from major blogging domains in the dataset and extract the social graph among their users. We also include a script to collect metadata from the most popular YouTube videos shared in blogs. Results from the analysis of this data were presented at ICWSM 2009’s Data Challenge.
- spinner-scripts.tar.gz (4.5 MB, 19 May 2009)
SL benchmarks
A set of benchmarks to evaluate separation logic (SL) entailment checkers as described at PLDI 2011. Includes benchmarks in formats suitable for Smallfoot, jStar, SLP, and theorem provers using the tptp format.
- slp-benchmarks.tgz (3.6 MB, 7 Apr 2011)
EPR benchmarks
A set of effectively propositional (EPR) formulas in the tptp format that can be used as benchmarks for first-order provers or provers specialised in this fragment. Implements the techniques described in Essays in Memory of Harald Ganzinger.
- epr.tar.gz (213 KB, 2 Aug 2007)
SMV to TPTP
The implementation of a tool to translate (bounded) model checking problems
described in the SMV language into an effectively propositional formula
using the tptp syntax. It implements the encoding approach described in
CADE 2007.
Supports boolean and enumerated types, modules and references to modules, process modules (with limitations), and LTL specifications.
- smv2tptp.tgz (123 KB, 2 Aug 2007)
Hard SAT
The implementation of the approach described at AAAI 2005 to randomly generate difficult-to-solve non-clausal propositional satisfiability (SAT) problems.
- genbal.tar.gz (16 KB, 24 Mar 2005)