Interpolant-based transition relation approximation

DOI10.1007/11513988_6MaRDI QIDQ5716597zbMATH OpenOpenAlexFDO

Authors Ranjit Jhala, K. L. McMillan

Publication date 10 January 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b138445

Mathematics Subject Classification ID

Theory of software (68N99) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Interpolant-Based Transition Relation Approximation
• Interpolant strength
• Approximation Refinement for Interpolation-Based Model Checking
• Abstractions from proofs
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(24)

• Farkas-based tree interpolation
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• Whale: an interpolation-based algorithm for inter-procedural verification
• Satisfiability modulo theories
• Transfer of model checking to industrial practice
• Verifying Reference Counting Implementations
• Interpolant strength
• SAT-based verification for timed component connectors
• Resolution proof transformation for compression and interpolation
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Ground Interpolation for Combined Theories
• Interpolant-Based Transition Relation Approximation
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Interpolation and symbol elimination in Vampire
• Tools and Algorithms for the Construction and Analysis of Systems
• Constraint solving for interpolation
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• Transition power abstractions for deep counterexample detection
• On symbol elimination and uniform interpolation in theory extensions
• On the completeness of interpolation algorithms
• Interpolation and SAT-based model checking revisited: adoption to software verification
• Completeness of interpolation algorithms in classical and non-classical logics
• Efficient generation of small interpolants in CNF
• Optimization techniques for Craig interpolant compaction in unbounded model checking

This page was built for publication: Interpolant-based transition relation approximation

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