Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
From MaRDI portal
Publication:2058375
DOI10.1007/s10703-021-00372-6OpenAlexW3163415025WikidataQ113902755 ScholiaQ113902755MaRDI QIDQ2058375
Peter Backeman, Philipp Rümmer, Aleksandar Zeljić
Publication date: 8 December 2021
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-021-00372-6
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Guiding Craig interpolation with domain-specific abstractions
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- SAT modulo linear arithmetic for solving polynomial constraints
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Efficient interpolation for the theory of arrays
- On interpolation in automated theorem proving
- Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
- An interpolating theorem prover
- Generating Non-linear Interpolants by Semidefinite Programming
- Quantifier-Free Interpolation of a Theory of Arrays
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Solving SAT and SAT Modulo Theories
- Ground Interpolation for the Theory of Equality
- Interpolant Strength
- Presburger arithmetic with unary predicates is Π11 complete
- Solving Polynomial Systems Using a Branch and Prune Approach
- Interpolation and Symbol Elimination
- Function Summarization Modulo Theories
- The MathSAT5 SMT Solver
- Synthesis of Circular Compositional Program Proofs via Abduction
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Complete instantiation-based interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Correct Hardware Design and Verification Methods
