Juan Antonio Navarro Pérez


Asterix: Separation Logic Prover. A theorem prover for separation logic entailments [aplas13]. Based on a model-based approach that leverages on SMT proving to reason about heap properties. The latest version won the 2014 SL-COMP theorem proving competition in the categories with acyclic list segments.

  • Binaries available upon request


DAHL: Distributed Systems in Prolog. A Prolog-based compiler and 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.


Cardan: 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 described in [cav09].


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].


Separation Logic

A set of benchmarks used to evaluate several separation logic entailment checkers in [pldi11]. Includes benchmarks in formats suitable for Smallfoot, jStar, SLP and theorem provers (TPTP).

Effectively Propositional Logic

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.

SMV to TPTP translator

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

Hard non-clausal satisfiability problems

The implementation of the model described in [aaai05] to randomly generate difficult to solve non-clausal propositional satisfiability problems.