Interpolation Procedure for Linear Arithmetic and Equality with Uninterpreted Function Symbols
CSIsat
is an interpolating decision procedure for the quantifier-free theory
of rational linear arithmetic and equality with uninterpreted function
symbols. Our implementation combines the efficiency of linear
programming for solving the arithmetic part with the efficiency of a
SAT solver to reason about the boolean structure.
The name CSIsat was chosen to reflect the architecture of the tool: Constraint-Solving based Interpolation combined with a SAT solving engine.
Authors/Maintainers: Dirk Beyer and Damien Zufferey
Current version: Check out from repository (or browse through).
CSIsat 1.2 (2008-07-08): Download zipped source code, or Browse through repository,
or download binaries for GNU/Linux x86 and x86_64, as well as for Win32/Cygwin.
Benchmarks used in our CAV'08 tool paper submission (browse directory)
(includes formulas, executables, benchmark scripts).
Project page available at Google Code: http://csisat.googlecode.com/
(includes source-code repository and downloads).
Valuable discussions relating to interpolation: Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani
(check out their TACAS'08 paper on interpolation)
Bug reports:
Erkan Keremoglu (Simon Fraser University, Canada), Jun 2008
Hiroshi Unno (University of Tokyo, Japan), Oct 2008
Performance Comparison (as of January 2008)
So far there are two other publicly available interpolation tools (this reflects the situation in April 2008):
CLPprover is an interpolation procedure for conjunctions of
linear-arithmetic inequalities and uninterpreted function symbols,
based on linear-constraint solving, implemented on top of the clp(q,r)
library in SICStus Prolog.
FOCI is an interpolation procedure for boolean combinations of linear-difference expressions over integers and equality with uninterpreted function symbols, implemented using proof-based methods.
Program
FOCI
CLPprover
CSIsat
kbfiltr
0.44
2.55
0.25
floppy
1.74
10.91
1.16
diskperf
0.87
5.40
0.56
cdaudio
0.94
5.94
0.60
alias/swap.c
0.07
13.20
0.06
The experiments were performed on a GNU/Linux x86_64 machine with an
Intel Core 2 Duo processor and 2 GB RAM, the processor was limited to 1
GHz to emphasize the difference. The table reports the run times of the
three tools on interpolation queries that occur during verification
processes of different programs. The first column identifies the
programs that were verified (by BLAST). During a verification run, we
dumped all interpolation queries to files. Then we ran the
interpolation procedures once again only on the queries, and the time
in the table is the sum of the run times over all queries that were
dumped for the program. The first four programs are MS Windows device
drivers, and the last one is from BLAST's regression test base (this
program requires interpolants for formulas with disjunctions, because
it uses pointer aliases).
The figure shows a comparative presentation of the results from
applying CLPprover and CSIsat to fragments of linear-arithmetic benchmarks from the SMT web site.
The time is given in seconds on a logarithmic scale. The total sum of
the run times for all examples is 75 min for CLPprover and 5.30 s for
CSIsat. The timeout was set to 600 s for this set of experiments. The
processor was running at 2.33 GHz.
