Nested interpolants

DOI10.1145/1706299.1706353zbMath1312.68059OpenAlexW2293685560MaRDI QIDQ5255103

Matthias Heizmann, Jochen Hoenicke, Andreas Podelski

Publication date: 11 June 2015

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

Full work available at URL: https://doi.org/10.1145/1706299.1706353

zbMATH Keywords

recursionstatic analysisabstract interpretationabstraction refinementFloyd-Hoare logicnested wordsinterpolantssoftware model checking

Mathematics Subject Classification ID

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

Related Items (20)

A complete refinement procedure for regular separability of context-free languages ⋮ Ramsey-Based Inclusion Checking for Visibly Pushdown Automata ⋮ Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ Proof tree preserving tree interpolation ⋮ Predicate Abstraction for Program Verification ⋮ Visibly pushdown transducers ⋮ Efficient modular SMT-based model checking of pointer programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Complete instantiation-based interpolation ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Farkas-based tree interpolation ⋮ Minimization of Visibly Pushdown Automata Using Partial Max-SAT ⋮ Horn clause verification with convex polyhedral abstraction and tree automata-based refinement ⋮ SMT-based model checking for recursive programs ⋮ What’s Decidable About Program Verification Modulo Axioms? ⋮ Automated Program Verification ⋮ On recursion-free Horn clauses and Craig interpolation ⋮ Domains for Higher-Order Games

This page was built for publication: Nested interpolants