Authors: Liam O'Reilly (1), Yoshinao Isobe (2), Markus Roggenbach (1) Affiliations: (1) University of Wales Swansea, United Kingdom (2) AIST, Tsukuba, Japan Title: Integrating Theorem Proving for Processes and Data - A State-of-the-art Report of an ongoing PhD Project Abstract: Distributed applications such as flight booking systems, web services, electronic payment systems, require parallel processing of data. Consequently, such systems have concurrent aspects (e.g. deadlock-freedom) as well as data aspects (e.g. functional correctness). Often, these aspects depend on each other. In [1], we designed the language CSP-CASL, which is tailored to the specification of distributed systems. There, we identified four basic integration problems, illustrated them by prototypical examples, and showed that CSP-CASL can cope with them. Here, we develop theorem proving support for CSP-CASL by translating CSP-CASL specifications into the input language of the already established tool CSP-Prover. Part of this translation is carried out by the tool HETS. At the current state of our project, we focus on the prototypical examples stated in [1]. As simple as they are, they capture the very nature of the integration problem between processes and data. It turns out that a systematic analysis of these specifications leads to a set of automatically provable theorems. With these theorems available, reasoning about CSP-CASL specifications becomes as easy as reasoning with CSP-Prover alone. [1] M.Roggenbach: CSP-CASL - A New Integration of Process Algebra and Algebraic Specification, TCS, Volume 354, 2006.