Verification of JCSP Programs.

We describe the rst proof system for concurrent programs based on Com- municating Sequential Processes for Java (JCSP). The system extends a complete cal- culus for the JavaCard Dynamic Logic with support for JCSP, which is modeled in terms of the CSP process algebra. Together with a novel efcient 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.