Nested interpolants

DOI10.1145/1706299.1706353zbMATH Open1312.68059OpenAlexW2293685560MaRDI QIDQ5255103FDOQ5255103

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

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

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)

Cited In (25)

• Title not available (Why is that?)
• A complete refinement procedure for regular separability of context-free languages
• 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
• Complete instantiation-based interpolation
• Regular separability of well-structured transition systems
• Efficient modular SMT-based model checking of pointer programs
• Trace Abstraction-Based Verification for Uninterpreted Programs
• Title not available (Why is that?)
• 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
• What's decidable about program verification modulo axioms?
• Minimization of visibly pushdown automata using partial Max-SAT

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)