CSIsat swMATH ID: 11407 Software Authors: Dirk Beyer; Damien Zufferey; Rupak Majumdar 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; Wolverine; SIMPLIFY; z3; BLAST; Yices; OpenSMT; SDPT3; Houdini; FAST; Eldarica; PeRIPLO; CPAchecker; FLATA; Chaff; Caduceus; SLAB; Why3; KRAKATOA Cited in: 14 Publications all top 5 Cited by 34 Authors 3 Kröning, Daniel 3 Rümmer, Philipp 2 Jung, Yungbum 2 Lee, Wonchan 2 Leroux, Jérôme 2 Rybalchenko, Andrey 2 Wang, Bow-Yaw 2 Yi, Kwangkeun 1 Bonacina, Maria Paola 1 Brillout, Angelo 1 Bruttomesso, Roberto 1 Chen, Mingshuai 1 Cimatti, Alessandro 1 Dai, Liyun 1 Gan, Ting 1 Ghilardi, Silvio 1 Goel, Amit 1 Griggio, Alberto 1 Johansson, Moa 1 Kapur, Deepak 1 Krstic, Sava A. 1 Mandrykin, M. U. 1 Mutilin, V. S. 1 Ranise, Silvio 1 Sebastiani, Roberto 1 Shved, P. E. 1 Sofronie-Stokkermans, Viorica 1 Subotic, Pavle 1 Tinelli, Cesare 1 Totla, Nishant 1 Wahl, Thomas 1 Wies, Thomas 1 Xia, Bican 1 Zhan, Naijun all top 5 Cited in 6 Serials 4 Journal of Automated Reasoning 1 Acta Informatica 1 Programming and Computer Software 1 Journal of Symbolic Computation 1 ACM Transactions on Computational Logic 1 Logical Methods in Computer Science Cited in 4 Fields 14 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) Citations by Year