A Quantifier Elimination Algorithm for Linear Real Arithmetic
David Monniaux (VERIMAG - Imag)

TL;DR
This paper introduces a new quantifier elimination algorithm for linear real arithmetic that leverages satisfiability modulo theory, demonstrating superior performance on program analysis examples compared to existing methods.
Contribution
The paper presents a novel quantifier elimination algorithm that effectively solves problems in linear real arithmetic using satisfiability modulo theory as a subroutine.
Findings
Successfully solves examples that other methods cannot
Outperforms existing implementations on program analysis problems
Demonstrates practical efficiency in real-world applications
Abstract
We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutine satisfiability modulo this theory, a problem for which there are several implementations available. The quantifier elimination algorithm presented in the paper is compared, on examples arising from program analysis problems, to several other implementations, all of which cannot solve some of the examples that our algorithm solves easily.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Numerical Methods and Algorithms
