We have released a new version of CafeOBJ. It includes fixes to the wrapper on Unix/Mac so that it can deal with spaces in paths. Furthermore, the ls command is now supported on Windows (but not on UNC path). The binary builds for 1.5.1 contain already all the fixes, so […]
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, […]
A case study for meta-level specifications Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time JAIST Collaboration Room 6 (I57-g) 2014/08/07 (Thu) 15:00 to 17:00 Abstract We provide an innovative development of algebraic specifications and proof scores in CafeOBJ by extending a base specification to the meta-level that […]
Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time 14th International Workshop on Termination July 2014, Vienna, Austria. Abstract We provide an innovative development of algebraic specifications and proof scores in CafeOBJ of QLock’s safety and liveness properties. The particular interest of the development is two-fold: Firstly, it […]
Lecturer Kokichi Futatsugi JAIST, Research Center for Software Verification, Japan Place/Time JAIST Collaboration Room 6 (I57-g) 2014/07/03 (Thu) 15:00 to 17:00 Abstract A new method for verification of transition systems is presented. The state space of a transition system is defined as a quotient set (i.e. a set of equivalence […]
