Simon Fraser University (SFU)

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

Authors/Maintainers: Dirk Beyer and Damien Zufferey

- CSIsat is free software (Apache 2.0 License)

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

(includes source-code repository and downloads).

- Tool paper at CAV 2008: CSIsat: Interpolation for LA+EUF

- API and source code documentation
- Tutorial coming soon
- Quick reference

- Browse through the source code

- Conceptual contributions: Rupak Majumdar
- 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

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

Author: Dirk Beyer, other project pages: BLAST, CCVisu, Chic, CrocoPat, CSIsat, Rabbit

Last updated: $Date: 2008-12-19 01:06:31 $ by $Author: beyer $