home
 scope
 programme
 venue
 award
 sponsors and organizers
 photo gallery
 participants





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:
  1. How many (one or two) problems are solved, and
  2. How well the problems are solved.

    Instructions

    • Deadline: July 31 (Thursday), 2008
    • Send your report via e-mail:
      • USE CARBON COPY or COPY facility of e-mail system and KEEP A COPY AT YOUR HAND. The copy should be an evidence of your submission, if your mail is lost in delivery.
      • The header of your email should be as follows:
        • To: kokichi@jaist.ac.jp, ogata@jaist.ac.jp, masaki-n@jaist.ac.jp, daniel@jaist.ac.jp
        • Cc:  <your email address>
        • Subject:  Sinaia School Award
    • Advices in preparing CafeOBJ codes:
      • The answers for the problems should at least contain CafeOBJ  specifications and proof scores.
      • Prepare files of the CafeOBJ codes following the file structure of ABP case study (Lecture Note 7).

     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): 63-75, 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.