Model-checking processes with data

We propose a procedure for automatically verifying properties (expressed in an extension of the modal image-calculus) over processes with data, specified in imageCRL. We first briefly review existing work, such as the theory of imageCRL and we discuss the logic, called first order modal image-calculus in more detail. Then, we introduce the formalism of first order boolean equation systems and focus on several lemmata that are at the basis of the soundness of our decision procedure. We discuss our findings on three non-trivial applications for a prototype implementation of this procedure. The results show that our prototype can deal with quite complex and interesting properties and systems, showing the efficacy of the approach.