CSIsat
swMATH ID: | 11407 |
Software Authors: | Beyer, Dirk; Zufferey, Damien; Majumdar, Rupak |
Description: | CSIsat: Interpolation for LA+EUF. We present CSIsat, 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. We evaluate the efficiency of our tool on benchmarks from software verification. Binaries and the source code of CSIsat are publicly available as free software. |
Homepage: | http://www.sosy-lab.org/~dbeyer/CSIsat/ |
Related Software: | FOCI; Princess; SyPet; Wolverine; SIMPLIFY; z3; BLAST; Yices; OpenSMT; SDPT3; SICStus; ARMC; PeRIPLO; Houdini; FAST; Eldarica; CPAchecker; FLATA; Chaff; Caduceus |
Cited in: | 16 Documents |
all
top 5
Cited by 36 Authors
all
top 5
Cited in 6 Serials
Cited in 4 Fields
16 | Computer science (68-XX) |
10 | Mathematical logic and foundations (03-XX) |
2 | Operations research, mathematical programming (90-XX) |
1 | General and overarching topics; collections (00-XX) |