Complete instantiation-based interpolation

DOI10.1145/2429069.2429132zbMath1301.68106OpenAlexW1964621354MaRDI QIDQ5891935

Nishant Totla, Thomas Wies

Publication date: 27 November 2014

Published in: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.295.8370

zbMATH Keywords

data structuresprogram analysisdecision proceduresCraig interpolantssatisfiability module theories

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Interpolation, preservation, definability (03C40)

Related Items

Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Proof tree preserving tree interpolation ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ Complete instantiation-based interpolation ⋮ Parametrized invariance for infinite state processes ⋮ On Interpolation and Symbol Elimination in Theory Extensions