Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.

DOI10.4230/LIPIcs.RTA.2011.171zbMath1236.68179arXiv1204.2386OpenAlexW1509079171MaRDI QIDQ5389080

Silvio Ranise, Roberto Bruttomesso, Silvio Ghilardi

Publication date: 24 April 2012

Full work available at URL: https://arxiv.org/abs/1204.2386

zbMATH Keywords

interpolationmodel-checkingrewritingarrays

Mathematics Subject Classification ID

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

Related Items (7)

Splitting via Interpolants ⋮ A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints ⋮ Interpolation and Model Checking ⋮ Complete instantiation-based interpolation ⋮ On Interpolation in Decision Procedures ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Quantifier-free interpolation in combinations of equality interpolating theories

Uses Software

• Princess
• OpenSMT

This page was built for publication: Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.