Talk


Proving liveness properties using abstract state machines and n-visibility

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


Liveness properties in CafeOBJ

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


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


Generate & Check Method in CafeOBJ Revised

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