Specification and verification of a simplified cloud synchronization protocol. Arbitrary many PCs can connect to a central cloud, fetch the value from the cloud, compare it with their own value, and update the cloud or their own value depending on which is larger. A detailed explanation can be found in a (part of) a presentation I gave during a work meeting: cloudsync.pdf.


The CafeOBJ specification and proof score are both available in

An independent implementation and verification of this protocol has been done in Constructor-based Inductive Theorem Prover (CITP) by Daniel Gaina.

Leave a comment

Your email address will not be published. Required fields are marked *