Juan Antonio Navarro Pérez

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.

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.

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.

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.

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.

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.

Hard SAT

The implementation of the approach described at AAAI 2005 to randomly generate difficult-to-solve non-clausal propositional satisfiability (SAT) problems.