Interpolation Results for Arrays with Length and MaxDiff
From MaRDI portal
Publication:6082222
DOI10.1145/3587161OpenAlexW4324057024MaRDI QIDQ6082222
Deepak Kapur, Silvio Ghilardi, Alessandro Gianola, Unnamed Author
Publication date: 3 November 2023
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/3587161
Cites Work
- Unnamed Item
- Model-theoretic methods in combined constraint satisfiability
- Constraint solving for interpolation
- Amalgamation properties and interpolation theorems for equational theories
- Cardinality constraints for arrays (decidability results and applications)
- Efficient interpolation for the theory of arrays
- NP satisfiability for arrays as powers
- Interpolation and amalgamation for arrays with MaxDiff
- Solving and interpolating constant arrays based on weak equivalences
- On Interpolation and Symbol Elimination in Theory Extensions
- Quantifier-Free Interpolation of a Theory of Arrays
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Interpolation in Local Theory Extensions
- Interpolation in local theory extensions
- Simplification by Cooperating Decision Procedures
- Proof Tree Preserving Interpolation
- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
- Quantifier-free interpolation in combinations of equality interpolating theories
- Constraint Solving for Interpolation
- Continuous Model Theory. (AM-58)
- Lazy Abstraction with Interpolants
- Complete instantiation-based interpolation
- Complete instantiation-based interpolation
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
This page was built for publication: Interpolation Results for Arrays with Length and MaxDiff
