Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking

DOI10.1007/s10703-022-00406-7MaRDI QIDQ6102162

Marco Palena, P. Pasini, Gianpiero Cabodi, P. E. Camurati

Publication date: 8 May 2023

Published in: Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

interpolationformal verificationSAT solvinghardware model checking

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Benchmarking a model checker for algorithmic improvements and tuning for performance
• Properties preserved in subdirect products
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• An abstraction algorithm for the verification of level-sensitive latch-based netlists
• SAT-Based Model Checking without Unrolling
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Counterexample-guided abstraction refinement for symbolic model checking
• Interpolant Strength
• Intertwined Forward-Backward Reachability Analysis Using Interpolants
• Approximation Refinement for Interpolation-Based Model Checking
• Correct Hardware Design and Verification Methods
• Computer Aided Verification
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

This page was built for publication: Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking