Monthly Archives: July 2014

Specifying and verifying liveness properties of QLOCK in CafeOBJ

This entry was posted in Event Talk on by

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 […]

Generate & Check Method in CafeOBJ Revised

This entry was posted in Event Talk on by

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 […]