We have released a new version of CafeOBJ. The only fix included in this point release is support for UNC path on Windows. Furthermore, we now provide experimental SBCL based Windows builds. Please see the download page for the new releases.
A case study for meta-level specifications Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time LOPSTR 2014: Logic-Based Program Synthesis and Transformation September 2014, Canterbury, UK. Abstract We provide an innovative development of algebraic specifications and proof scores in CafeOBJ by extending a base specification to the meta-level […]
QLOCK, a variant of Dijkstra’s binary semaphore, is a well known protocol of mutual exclusion, and many implementation and verifications in CafeOBJ are available. I have extended the current proofs of mutual exclusion to cover also fairness, i.e., any agent will eventually enter the queue and eventually go into critical […]
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 […]
Yesterday we have finally released CafeOBJ 1.5.0. This marks a great step forward in a long development history of this algebraic specification and verification language. To quote from our README: CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its […]
Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time WADT 2014: 22nd International Workshop on Algebraic Development Techniques September 2014, Sinaia, Romania. Abstract One methodolgy for formal specification of a complex system is by using Abstract State Machine (Asm). Here states describe the actual state of the system, […]
