Princess

Theorem Proving in First-Order Logic modulo Linear Integer Arithmetic

Princess is a theorem prover for Presburger arithmetic with uninterpreted predicates. This means that Princess can reason about problems in integer arithmetic without multiplication (only multiplication with integer literals is allowed), augmented with predicates that can be axiomatised arbitrarily. Such problems can contain arbitrary quantifiers to express that some formula is supposed to hold for all or for some integers. Some further features of Princess include:

Princess is a decision procedure for formulae in Presburger arithmetic (without uninterpreted predicates) and can eliminate quantifiers
Handling of (partial and total) functions via an encoding into uninterpreted predicates
Extraction of Craig interpolants for valid formulae (with some restrictions on the use of quantifiers)
Triggers and e-matching for user-guided handling of quantified formulae, similar as in SMT solvers
Handling of the theory of arrays via user-specified axioms
Princess can read problems in its own native format, in the SMT-LIB 2 format, and in the FOF/TFF/CNF dialects of TPTP.
About performance: Princess won the TFA division (arithmetic problems) at CASC J6, 2012

You can run Princess using Java Webstart, provided that you have a Java runtime environment (version 1.5 or newer) and Webstart installed on your computer. Java Webstart is usually included in JREs. For example problems to be proven, see the tutorial page and the source distributions.

Princess is free software and distributed under GPL v3. The latest release is 2013-04-21.

Please contact me if you are interested in any projects or thesis work related to Princess. (possible topics)

Examples

Sources

Benchmarks

Documentation and Publications

Definition of the Princess syntax. Examples are included in the Princess distributions, and on the examples page
Documentation of the Princess sources. If you want to use the Princess API, you need to download a source distribution. It is then easiest to start from the class ap.SimpleAPI, and use the functions in ap.parser.IExpression to construct formulae. Examples are given in the file testcases/api/SimpleAPITest.scala.

LPAR paper about the calculus that is used in Princess
A more detailed description of the calculus and Princess is part of my PhD thesis
IJCAR paper on interpolant generation in Presburger arithmetic
VERIFY and VMCAI papers on interpolant generation in the presence of uninterpreted predicates, functions, and arrays
LPAR paper about e-matching and the handling of functions in Princess
Talk about Princess that I gave at Microsoft Research Redmond.
Talk about E-Matching in Princess that I gave at the wintermeeting of the SET division at Chalmers University
The native input format of Princess much resembles the format that is used by the KeY tool. You can have a look at the example files that are included in the distributions below.
There is also a converter (based on SMT-LIB parser 2.0 by Mike Decoster and Michael Schidlowsky) from the SMT-LIB 1 format to the Princess format. Note that Princess is by now able to directly read problems in the SMT-LIB 2 format.

Applications

Here is a (probably incomplete) list of applications of Princess that I am aware of. I am interested in learning about further situations where Princess was found to be useful, so in case you have one feel free to drop me a mail!

Seneschal, a ranking function generator for bitvector relations
Eldarica, a predicate abstraction-based model checker
Joogie, a tool for detection of infeasible code in Java applications
Picasso, a static analyzer for depth-bounded systems

Installation of the binary distribution

We provide a binary distribution of the latest version of Princess. This distribution contains all required libraries, i.e., the Scala API and the Cup parser generator library; it is only necessary to have a Java runtime environment (version 1.5 or newer) installed.

To install, just download the archive and unpack it in some directory of your choice. The Princess gui can then be invoked using the script princessGui, the command line tool using the script princess.

Compilation, Installation from source

The compilation is so far only tested on Linux systems. For the installation, you need:

A compiler for Scala version 2.10 or newer
A Java SDK version 1.5 or newer
The Cup parser generator for Java (get the file java-cup-11a.jar)
If you want to compile the parser yourself (binaries are included in the Princess snapshots below), you also need the BNF converter and JLex.

The actual installation consists of the following steps:

Unpack one of the snapshots (preferably the newest one) and change to the princess-* directory
Create a directory extlibs and copy the file java-cup-11a.jar into it
In case you want to compile the parser yourself (not necessary), run make parser-jar
Run make to compile Princess.

If everything went ok, it is possible to run Princess with the command ./princess <inputfile>
A list of the Princess options can be printed using ./princess -h