An Instantiation-Based Approach for Solving Quantified Linear Arithmetic

2015/10/09 by Andrew Reynolds, Reynolds, Andrew, Tim L. King +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Testing and Debugging Techniques

paper · pdf · doi:10.48550/arxiv.1510.02642

openalex publication_date 2015/10/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedures for linear real arithmetic (LRA) and linear integer arithmetic (LIA) formulas with one quantifier alternation. Our procedure can be integrated into the solving architecture used by typical SMT solvers. Experimental results on standardized benchmarks from model checking, static analysis, and synthesis show that our implementation of the procedure in the SMT solver CVC4 outperforms existing tools for quantified linear arithmetic.

Citations

• Simplify: a theorem prover for program checking

Cited by

• A Decision Procedure for Separation Logic in SMT

Related

• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• On using floating-point computations to help an exact linear arithmetic decision procedure
• Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
• Instantiation of SMT problems modulo Integers
• Quantifier Instantiations: To Mimic or To Revolt?