iPrincess is an interpolating theorem prover for Presburger arithmetic with uninterpreted predicates. The tool is able to prove or disprove the validity of formulae in this logic and, in case a formula is found to be valid, iPrincess is able to generate Craig interpolants for any two partitions of the formula.

The implementation is based on Princess which has been extended to generate proofs of validity. Our new algorithm recursively visits the proof and generates an interpolant using the rules presented in this paper.

You can run iPrincess 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 source distributions below. |

iPrincess is free software and distributed under GPL v3.

- IJCAR'10 paper about interpolation in quantifier-free Presburger arithmetic, as done in iPrincess.
- VERIFY-2010 paper about
interpolation in the theory of arrays.

- The Princess examples
explain the input format accepted by iPrincess.

- The input format of iPrincess 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.

The following results compare interpolation runtimes of iPrincess and Quantifier Elimination. Diagrams and a discussion of the benchmarks are given in our IJCAR paper. The benchmarks were run on an Intel Pentium Xeon with 3 GHz, using a timeout of 120s. The interpolation problems are derived from the QF_LIA category of SMT-LIB (quantifier-free formulae over linear integer arithmetic).

SMT-LIB
converter
(based on SMT-LIB parser 2.0

by Mike Decoster and Michael Schidlowsky)

- 31/08/2010: The functionality
of iPrincess has been backported and integrated into the standard Princess version; we do not plan to
separately continue development on iPrincess.

- 27/05/2010:
Updated
version
with many optimisations and fixes. The calculus has
been extended to support interpolation in quantifier-free Presburger
arithmetic with uninterpreted predicates, which also makes it possible
to handle uninterpreted functions and the theory of arrays. More
details are given in a paper
at the VERIFY-2010
workshop.

- 24/01/2010:
First
official
release of iPrincess

We recommend to use Princess instead of the older versions of
iPrincess on this page. As of August 2010, all functionality of
iPrincess is also available in Princess.

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

- A compiler for Scala
version 2.7

- 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 iPrincess snapshots below), you also need the BNF converter and JLex.

The actual installation consists of the following steps:

- Unpack one of the snapshots below (preferably the newest one) and
change to the
`iprincess-*`

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

If everything went ok, it is possible to run iPrincess with the
command `./princess <inputfile>`