Sciweavers

Share
ICCAD
2006
IEEE

Stepping forward with interpolants in unbounded model checking

10 years 3 months ago
Stepping forward with interpolants in unbounded model checking
This paper addresses SAT-based Unbounded Model Checking based on Craig Interpolants. This recently introduced methodology is often able to outperform BDDs and other SAT-based techniques on large verification instances. Based on refutation proofs generated by SAT solvers, interpolants provide compact circuit representations of state sets, and away several details non relevant for proofs. We propose three main contributions, aimed at controlling interpolant size and traversal depth. First of all, we introduce interpolant-based dynamic abstraction to reduce the support of the computed interpolant. Second, we propose new advances in interpolant compaction by redundancy removal. Both techniques rely on an effective application of the incremental SAT paradigm. Finally, we also introduce interpolant computation exploiting circuit quantification, instead of SAT refutation proofs. Experimental results are specifically oriented to prove properties, rather than disproving them (bug hunting). ...
Gianpiero Cabodi, Marco Murciano, Sergio Nocco, St
Added 11 Jun 2010
Updated 11 Jun 2010
Type Conference
Year 2006
Where ICCAD
Authors Gianpiero Cabodi, Marco Murciano, Sergio Nocco, Stefano Quer
Comments (0)
books