Approximation Refinement for Interpolation-Based Model Checking

DOI10.1007/978-3-540-78163-9_10zbMATH Open1138.68444OpenAlexW1805082449MaRDI QIDQ5452708FDOQ5452708

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

Recommendations

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (14)

• Interpolant-Based Transition Relation Approximation
• Interpolation and model checking
• Accelerating Interpolation-Based Model-Checking
• Widening and narrowing operators for abstract interpretation
• Interpolation and SAT-based model checking.
• Correct Hardware Design and Verification Methods
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• Efficient generation of small interpolants in CNF
• 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)