6533b7defe1ef96bd1275bfd

RESEARCH PRODUCT

Improving Interpolants for Linear Arithmetic

Björn BeberJoschka KupilasChristoph SchollErnst AlthausErnst Althaus

subject

AlgebraReduction (complexity)Linear programmingHeuristicModuloCraig interpolationArithmeticFormal verificationSatisfiabilityLocal search (constraint satisfaction)Mathematics

description

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.

yearjournalcountryeditionlanguage
2015-01-01
https://doi.org/10.1007/978-3-319-24953-7_5