A CONSTRAINT-BASED TRANSFORMATION FOR VERIFYING INFINITE STATE SYSTEMS

We address the problem of verifying safety properties of infinite state reactive systems that use unbounded integer variables. We consider systems specified by using linear constraints over the integers and we assume that, for verifying safety properties of these systems, one uses reachability analysis techniques. Our method improves the effectiveness of forward and backward reacha-bility analyses by preprocessing the system specification. For forward reachability our method consists in: (i) transforming the system specification into an equivalent one (with respect to the safety property of interest) by a constraint propagation technique that works backward from the constraints representing the unsafe states, and then (ii) applying to the transformed system specification a reachability analysis that works forward from the constraints representing the initial states. For backward reachability our method works as for forward reachability, by inter-changing the roles of the initial states and the unsafe states. We have implemented our metho