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

This paper addresses model checking based on SAT solvers and Craig interpolants. We tackle major scalability problems of state-of-the-art interpolation-based approaches, and we achieve two main results: (1) A novel model checking algorithm; (2) A new and flexible way to handle an incremental represe...

Full description

Saved in:
Bibliographic Details
Published in:Formal methods in system design 2022-04, Vol.60 (2), p.117-146
Main Authors: Cabodi, G., Camurati, P. E., Palena, M., Pasini, P.
Format: Article
Language:English
Subjects:
Algorithms
CAE) and Design
Circuits and Systems
Computer-Aided Engineering (CAD
Data structures
Electrical Engineering
Engineering
Interpolation
Software Engineering/Programming and Operating Systems
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper addresses model checking based on SAT solvers and Craig interpolants. We tackle major scalability problems of state-of-the-art interpolation-based approaches, and we achieve two main results: (1) A novel model checking algorithm; (2) A new and flexible way to handle an incremental representation of (over-approximated) forward reachable states. The new model checking algorithm IGR, Interpolation with Guided Refinement, partially takes inspiration from IC3 and interpolation sequences. It bases its robustness and scalability on incremental refinement of state sets, and guided unwinding/simplification of transition relation unrollings. State sets, the central data structure of our algorithm, are incrementally refined, and they represent a valuable information to be shared among related problems, either in concurrent or sequential (multiple-engine or multiple-property) execution schemes. We provide experimental data, showing that IGR extends the capability of a state-of-the-art model checker, with a specific focus on hard-to-prove properties.
ISSN:0925-9856
1572-8102
DOI:10.1007/s10703-022-00406-7