Interpolation and amalgamation for arrays with MaxDiff

DOI10.1007/978-3-030-71995-1_14OpenAlexW3136627104MaRDI QIDQ2233410FDOQ2233410

Authors: Silvio Ghilardi, Alessandro Gianola, Deepak Kapur 

Publication date: 18 October 2021

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

zbMATH Keywords

interpolationSMTamalgamationarrays

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites Work

• Booster: an acceleration-based verification framework for array programs
• Simplification by Cooperating Decision Procedures
• Interpolation and SAT-based model checking.
• Model theory.
• 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
• Interpolation in local theory extensions
• Lower bounds for resolution and cutting plane proofs and monotone computations
• An extension of lazy abstraction with interpolation for programs with arrays
• Quantifier-free interpolation in combinations of equality interpolating theories
• Lazy Abstraction with Interpolants
• Verification, Model Checking, and Abstract Interpretation
• Model-theoretic methods in combined constraint satisfiability
• Amalgamation properties and interpolation theorems for equational theories
• Verifying array manipulating programs with full-program induction
• Putting the squeeze on array programs: loop verification via inductive rank reduction
• Efficient interpolation for the theory of arrays
• Quantifiers on demand
• Interpolation, amalgamation and combination (the non-disjoint signatures case)
• Conditional congruence closure over uninterpreted and interpreted symbols
• Modularity results for interpolation, amalgamation and superamalgamation
• From model completeness to verification of data aware processes
• Model completeness, covers and superposition
• Complete instantiation-based interpolation
• Interpolation and amalgamation for arrays with MaxDiff

Cited In (3)

• Interpolation and amalgamation for arrays with MaxDiff
• Reasoning about vectors: satisfiability modulo a theory of sequences
• Interpolation Results for Arrays with Length and MaxDiff

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)