Skip to main content
Conference ProceedingsOPEN ACCESS

CSISAT: Interpolation for LA+EUF: Tool paper

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2008) 5123 LNCS 304-308
DOI: 10.1007/978-3-540-70545-1_29
38Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

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. © 2008 Springer-Verlag.

Cite

CITATION STYLE

APA

Beyer, D., Zufferey, D., & Majumdar, R. (2008). CSISAT: Interpolation for LA+EUF: Tool paper. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5123 LNCS, pp. 304–308). https://doi.org/10.1007/978-3-540-70545-1_29

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free