Craig interpolation for satisfiability modulo theory formulas have come more into focus for applications of formal verification. In this paper we, introduce a method to reduce the size of linear constraints used in the description of already computed interpolant in the theory of linear arithmetic with respect to the number of linear constraints. We successfully improve interpolants by combining satisfiability modulo theory and linear programming in a local search heuristic. Our experimental results suggest a lower running time and a larger reduction compared to other methods from the literature.
CITATION STYLE
Althaus, E., Beber, B., Kupilas, J., & Scholl, C. (2015). Improving interpolants for linear arithmetic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9364, pp. 48–63). Springer Verlag. https://doi.org/10.1007/978-3-319-24953-7_5
Mendeley helps you to discover research relevant for your work.