2008/03/11 by David Monniaux, Monniaux, David
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Numerical Methods and Algorithms
paper · doi:10.48550/arxiv.0803.1575
openalex publication_date 2008/03/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.