Nested interpolants

DOI10.1145/1706299.1706353MaRDI QIDQ5255103zbMATH OpenOpenAlexFDO

Authors 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

abstract interpretationabstraction refinementrecursionstatic analysisFloyd-Hoare logicnested wordsinterpolantssoftware model checking

Mathematics Subject Classification ID

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

Recommendations

• Lazy Abstraction with Interpolants
• scientific article; zbMATH DE number 5245252
• Model Checking: From Tools to Theory
• Interpolants and Symbolic Model Checking
• Adding nesting structure to words

Cited in

(25)

• Minimization of visibly pushdown automata using partial Max-SAT
• What's decidable about program verification modulo axioms?
• A complete refinement procedure for regular separability of context-free languages
• scientific article; zbMATH DE number 7447757 (Why is no real title available?)
• Domains for Higher-Order Games
• Dynamic nested brackets
• Whale: an interpolation-based algorithm for inter-procedural verification
• Automated program verification
• Farkas-based tree interpolation
• Proof tree preserving tree interpolation
• Predicate abstraction for program verification
• On recursion-free Horn clauses and Craig interpolation
• Interpolation in nest algebra modules
• Regular separability of well-structured transition systems
• Complete instantiation-based interpolation
• Efficient modular SMT-based model checking of pointer programs
• Trace Abstraction-Based Verification for Uninterpreted Programs
• scientific article; zbMATH DE number 7444022 (Why is no real title available?)
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
• Learning inductive invariants by sampling from frequency distributions
• Ramsey-based inclusion checking for visibly pushdown automata
• Antichains algorithms for the inclusion problem between \(\omega\)-VPL
• SMT-based model checking for recursive programs
• Visibly pushdown transducers
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

This page was built for publication: Nested interpolants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5255103)