FAR-Cubicle - A new reachability algorithm for Cubicle

Sylvain Conchon, Amit Goel, Sava Krstic +2

We present a fully automatic algorithm for verifying safety properties of parameterized software systems. This algorithm is based on both IC3 and Lazy Annotation. We implemented it…