Interpolation and amalgamation for arrays with MaxDiff
From MaRDI portal
Publication:2233410
DOI10.1007/978-3-030-71995-1_14OpenAlexW3136627104MaRDI QIDQ2233410
Deepak Kapur, Alessandro Gianola, Silvio Ghilardi
Publication date: 18 October 2021
Full work available at URL: https://arxiv.org/abs/2010.07082
Related Items (3)
Reasoning about vectors: satisfiability modulo a theory of sequences ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ Interpolation and amalgamation for arrays with MaxDiff
Cites Work
- An extension of lazy abstraction with interpolation for programs with arrays
- Model-theoretic methods in combined constraint satisfiability
- Putting the squeeze on array programs: loop verification via inductive rank reduction
- Model theory.
- Amalgamation properties and interpolation theorems for equational theories
- Interpolation, amalgamation and combination (the non-disjoint signatures case)
- Conditional congruence closure over uninterpreted and interpreted symbols
- Efficient interpolation for the theory of arrays
- From model completeness to verification of data aware processes
- Interpolation and amalgamation for arrays with MaxDiff
- Model completeness, covers and superposition
- Modularity results for interpolation, amalgamation and superamalgamation
- On Interpolation and Symbol Elimination in Theory Extensions
- Quantifier-Free Interpolation of a Theory of Arrays
- Lazy Abstraction with Interpolants for Arrays
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Booster: An Acceleration-Based Verification Framework for Array Programs
- Interpolation in local theory extensions
- Simplification by Cooperating Decision Procedures
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Verifying Array Manipulating Programs with Full-Program Induction
- Quantifier-free interpolation in combinations of equality interpolating theories
- Lazy Abstraction with Interpolants
- Complete instantiation-based interpolation
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Quantifiers on demand
This page was built for publication: Interpolation and amalgamation for arrays with MaxDiff
