

The authors of the best solutions to the problems proposed will be invited to JAIST, Japan with the full support of travelling and staying expenses. The evaluation will be done based on:
Instructions
Problem 1 Read the paper E. W. Dijkstra: Solution of a problem in concurrent programming control, CACM 8(9): 569, 1965. and make an OTS modeling the mutual exclusion protocol described in the paper, write a CafeOBJ specification of the OTS, and write proof scores that the protocol satisfies the mutual exclusion property. Problem 2 Read the paper K. Mani Chandy and Leslie Lamport: Distributed snapshots: determining global states of distributed systems, ACM TOCS 3(1): 6375, 1985. and make an OTS modeling the distributed snapshot algorithm, write a CafeOBJ specification of the OTS, conjecture some desired properties, write proof scores that the algorithm satisfies the properties. 