A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints

DOI10.1007/978-3-642-24364-6_8zbMATH Open1348.68123OpenAlexW194239260MaRDI QIDQ3172885FDOQ3172885

Authors Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

Publication date 7 October 2011

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24364-6_8

Mathematics Subject Classification ID

Data structures (68P05) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Rewriting-based quantifier-free interpolation for a theory of arrays
• Quantifier-free interpolation of a theory of arrays
• Efficient interpolation for the theory of arrays
• Constraint Solving for Interpolation
• Constraint solving for interpolation

Cites work

• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• Abstractions from proofs
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating theorem prover
• Automated Deduction – CADE-20
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Constraint Solving for Interpolation
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Ground Interpolation for the Theory of Equality
• Negative-cycle detection algorithms
• Rewriting-based quantifier-free interpolation for a theory of arrays
• Simplification by Cooperating Decision Procedures
• Term Rewriting and All That

Cited in

(6)

• Quantifier-free interpolation in combinations of equality interpolating theories
• Interpolation systems for ground proofs in automated deduction: a survey
• Efficient interpolation for the theory of arrays
• Quantifier-free interpolation of a theory of arrays
• Rewriting-based quantifier-free interpolation for a theory of arrays
• Solving and interpolating constant arrays based on weak equivalences

Describes a project that uses

Uses Software

• Princess
• OpenSMT
• FOCI

This page was built for publication: A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172885)