Intertwined forward-backward reachability analysis using interpolants

DOI10.1007/978-3-642-36742-7_22MaRDI QIDQ5326333zbMATH OpenOpenAlexFDO

Authors Yakir Vizel, Orna Grumberg, Sharon Shoham

Publication date 5 August 2013

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-36742-7_22

Mathematics Subject Classification ID

Logic in computer science (03B70) Interpolation, preservation, definability (03C40) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Interpolation and SAT-based model checking.
• Approximation Refinement for Interpolation-Based Model Checking
• Interpolant learning and reuse in SAT-based model checking
• Interpolation Properties and SAT-Based Model Checking
• Accelerating Interpolation-Based Model-Checking

Cited in

(5)

• Loop verification with invariants and contracts
• Combining model checking and data-flow analysis
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• SAT-based invariant inference and its relation to concept learning
• Efficient generation of small interpolants in CNF

This page was built for publication: Intertwined forward-backward reachability analysis using interpolants

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