Separation Logic Benchmarks
The set of benchmarks that were used to evaluate several separation logic entailment checkers in [pldi11]. Includes benchmarks in formats suitable for Smallfoot, jStar, SLP and theorem provers (TPTP).
- slp-benchmarks.tgz (3.5 MB, 7 Apr 2011)
DAHL: Distributed Systems in Prolog
DAHL is a Prolog-based compiler and a runtime environment for distributed applications [tplp10]. It aims to provide a high-level specification language in which network protocols can be described as Prolog queries that respond to messages received from the network.
Spinn3r Blog Data
A collection of the data that we extracted from the Spinn3er dataset. It includes data about all the posts from mayor blogging domains that were included in the dataset, as well as the extracted social graph among their corresponding blog users. We also include metadata that we collected from the most popular YouTube videos shared in blogs. More details and the analysis of this data has been published at [icwsm09].
- spinner.tar.gz (644MB, 29 Sep 2009)
- spinner-scripts.tar.gz (4.3MB, 19 May 2009)
Cardan Tool: Cardinality analysis for P2 programs
Binaries for Linux/x86 of the Cardan Tool to translate declarative rules of a P2 program into a transition relation suitable for model checking with ARMC. An updated binary of ARMC is also included. It is based on an abstraction approach descrived in [cav09].
- cardan.tar.gz (2.2 MB, 29 Jan 2009)
Benchmarks for effectively propositional provers
This is a set of effectively propositional formulas in the tptp syntax that can be used as benchmarks for first-order provers, or provers specialised in this fragment.
- epr.tar.gz (2 Aug 2007)
Translation of SMV descriptions to TPTP
This is the implementation of a tool to translate (bounded) model checking problems described in the SMV language, into effectively propositional formula using the tptp syntax. It is based on the encoding approach described in [cade07].
Currently the following SMV features are implemented:
- Boolean and enumerated types
- Modules and references to modules
- Limited support of process modules
- LTL specifications
Please note that this software is still at early development stages. For questions, comments and bug reports contact navarroj@cs.man.ac.uk.
- smv2tptp.tgz (2 Aug 2007)
Hard non-clausal satisfiability problems
This is the implementation of the model described in [aaai05] to randomly generate difficult to solve non-clausal propositional satisfiability problems.
- genbal.tar.gz (24 Mar 2005)