Verification of JCSP Programs
Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt · Chalmers Publication Library (Chalmers University of Technology) · 2005
We describe the first proof system for concurrent programs based on Communicating Sequential Processes for Java (JCSP). The system extends a complete calculus for the JavaCard Dynamic Logic with support for JCSP, which is modeled in terms of the CSP process algebra. Together with a novel efficient calculus for CSP, a rule system is obtained that enables JCSP programs to be executed symbolically and to be checked against temporal properties. The proof system has been implemented within the KeY tool and is publicly available.