Paper Info
Title
Improving Convergence Rate Of IC3.
Abstract
IC3, a well-known model checker, proves a property of a transition system by building a sequence of formulas $F_0,\dots,F_k$. Formula $F_i$, $0 \leq i \leq k$ over-approximates the set of states reachable in at most $i$ transitions. The basic algorithm of IC3 cannot guarantee that the value of $k$ never exceeds the reachability diameter of the system. We describe an algorithm called IC4 that gives such a guarantee. (IC4 stands for 'IC3 + Improved Convergence'). One can argue that the average convergence rate of IC4 is better than for IC3 as well. Improving convergence can facilitate some other variations of the basic algorithm. As an example, we describe a version of IC4 employing property decomposition. The latter means replacing an original (strong) property with a conjunction of weaker properties to prove by IC4. We argue that addressing the convergence problem is important for making the property decomposition approach work.
Year
Venue
Field
2018
arXiv: Logic in Computer Science
Convergence (routing),Discrete mathematics,Model checking,Reachability,Rate of convergence,Mathematics
DocType
Volume
Citations 
Journal
abs/1809.00503
0
PageRank 
References 
Authors
0.34
0
1
Name
Order
Citations
PageRank
Eugene Goldberg1258.01