Interpolation and amalgamation for arrays with MaxDiff
From MaRDI portal
Publication:2233410
Cites work
- Amalgamation properties and interpolation theorems for equational theories
- An extension of lazy abstraction with interpolation for programs with arrays
- Booster: an acceleration-based verification framework for array programs
- Complete instantiation-based interpolation
- 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 SAT-based model checking.
- Interpolation and amalgamation for arrays with MaxDiff
- Interpolation in local theory extensions
- Interpolation, amalgamation and combination (the non-disjoint signatures case)
- Lazy Abstraction with Interpolants
- Lazy abstraction with interpolants for arrays
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Model completeness, covers and superposition
- Model theory.
- Model-theoretic methods in combined constraint satisfiability
- Modularity results for interpolation, amalgamation and superamalgamation
- Putting the squeeze on array programs: loop verification via inductive rank reduction
- Quantifier-free interpolation in combinations of equality interpolating theories
- Quantifier-free interpolation of a theory of arrays
- Quantifiers on demand
- Simplification by Cooperating Decision Procedures
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Verification, Model Checking, and Abstract Interpretation
- Verifying array manipulating programs with full-program induction
Cited in
(3)
This page was built for publication: Interpolation and amalgamation for arrays with MaxDiff
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233410)
