Approximation Refinement for Interpolation-Based Model Checking

DOI10.1007/978-3-540-78163-9_10zbMath1138.68444OpenAlexW1805082449MaRDI QIDQ5452708

Daniel Kroening, Mitra Purandare, Vijay D'Silva

Publication date: 4 April 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-78163-9_10

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (3)

Optimization techniques for Craig interpolant compaction in unbounded model checking ⋮ Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking ⋮ Widening and narrowing operators for abstract interpretation

Cites Work

• Unnamed Item
• Unnamed Item
• From pre-historic to post-modern symbolic model checking
• Interpolant Learning and Reuse in SAT-Based Model Checking
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Fixpoint-Guided Abstraction Refinements
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Interpolant-Based Transition Relation Approximation
• Formal Methods in Computer-Aided Design
• Correct Hardware Design and Verification Methods
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

This page was built for publication: Approximation Refinement for Interpolation-Based Model Checking