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 extends base specifications in order-sorted and rewriting logics to a meta-level, which requires behavioral logic, thus using the three logics together to achieve the proofs. Secondly, we use a search predicate and covering state patterns that allow us to prove the validity of a property over all possible one-step transitions, by which safety and liveness properties in the base and meta-level can be proven.