Title:
Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation

Abstract:
In this talk we consider the problem of the automated verification of infinite state
reactive systems. To address this problem we propose a method based on the
specialization of constraint logic programs (CLP). Our verification method
applies to an encoding of an infinite state system as a CLP and consists of
a two-phase procedure: (1) in the first phase we specialize the system w.r.t.
the initial state and the property to be verified, and (2) in the second phase
the specialized system is evaluated by a bottom-up strategy. The novelty of our
approach with respect to other constraint-based verification techniques is in
the ability of exploiting the informations regarding both the initial states and
the property to be verified before using a backward analysis of the (specialized)
system. We illustrate the two phases and some generalization strategies that
ensure the termination of the method. Then, we discuss some experimental
results obtained using an implementation of our method in the MAP transformation
system. Using some benchmark examples, we compare our system with
the constraint-based verification tools ALV, DMC, and HyTech. The experimental
results show that our method is effective and competitive with respect to these
other tools.