An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic
Abstract elided by the publisher.
Related papers
- Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions CPP 2026
- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure CAV 2009
- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions TACAS 2015
- Automatic Verification of Pointer Programs using Monadic Second-Order Logic PLDI 1997
- Sets with Cardinality Constraints in Satisfiability Modulo Theories VMCAI 2011
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic TACAS 2011
- A Non-linear Arithmetic Procedure for Control-Command Software Verification TACAS 2018
- An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic TACAS 2003