Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
From MaRDI portal
Publication:5389080
DOI10.4230/LIPIcs.RTA.2011.171zbMath1236.68179arXiv1204.2386MaRDI QIDQ5389080
Silvio Ranise, Roberto Bruttomesso, Silvio Ghilardi
Publication date: 24 April 2012
Full work available at URL: https://arxiv.org/abs/1204.2386
68Q60: Specification and verification (program logics, model checking, etc.)
68Q42: Grammars and rewriting systems
Related Items
Quantifier-free interpolation in combinations of equality interpolating theories, Complete instantiation-based interpolation, Parallelizing SMT solving: lazy decomposition and conciliation, Splitting via Interpolants, On Interpolation in Decision Procedures, A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints, Interpolation and Model Checking
Uses Software