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 (see details).
- 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 2014-02-10.

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

- Manual of Princess (rather incomplete at the moment). Examples are included in the Princess distributions, and on the examples page.
- Definition of the Princess syntax.
- 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.

- 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

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`

.

We currently maintain a separate branch for full support of the TPTP format. You can download a binary of the latest version, or the sources. This version differs from normal Princess mainly in the following points:

- the default input format is chosen to be TPTP;
- by default, the prover runs with the option
`+multiStrategy`

, with a portfolio of strategies optimised for TPTP problems; - the semantics of uninterpreted sorts is different from the semantics assumed by standard Princess: in the standard version, uninterpreted sorts are always considered to be infinite (since they are internally mapped to the datatype of integers), whereas in the CASC version type guards are generated to correctly model also finite domains;
- results are output in the SZS notation.

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`