Specifying and verifying liveness properties of QLOCK in CafeOBJ
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 […]