Approximation Refinement for Interpolation-Based Model Checking

DOI10.1007/978-3-540-78163-9_10MaRDI QIDQ5452708zbMATH OpenOpenAlexFDO

Authors Vijay D'Silva, Mitra Purandare, Daniel Kroening

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)

Recommendations

• Computer Science Logic
• Interpolation and SAT-based model checking.
• Interpolation Properties and SAT-Based Model Checking
• Accelerating Interpolation-Based Model-Checking
• Interpolant strength

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1903372 (Why is no real title available?)
• Correct Hardware Design and Verification Methods
• Fixpoint-Guided Abstraction Refinements
• Formal Methods in Computer-Aided Design
• From pre-historic to post-modern symbolic model checking
• Interpolant learning and reuse in SAT-based model checking
• Interpolant-Based Transition Relation Approximation
• Interpolation and SAT-based model checking.
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(14)

• Interpolant-Based Transition Relation Approximation
• Interpolation and model checking
• Widening and narrowing operators for abstract interpretation
• Accelerating Interpolation-Based Model-Checking
• Interpolation and SAT-based model checking.
• Correct Hardware Design and Verification Methods
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• Efficient generation of small interpolants in CNF
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• Proof-guided underapproximation-widening for multi-process systems
• Intertwined forward-backward reachability analysis using interpolants
• Interpolation Properties and SAT-Based Model Checking
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems

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

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