Nested interpolants
From MaRDI portal
Publication:5255103
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
recursionstatic analysisabstract interpretationabstraction refinementFloyd-Hoare logicnested wordsinterpolantssoftware model checking
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
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
