Lecturer
Kokichi Futatsugi
JAIST, Research Center for Software Verification, Japan
Place/Time
JAIST IS school seminar room 9F
2015/02/26 (Thu) 15:00 to 17:00
Abstract
Generic proof scores for the generate & check method in CafeOBJ are presented. The generic proof scores codify the generate & check method as parameterized modules in the CafeOBJ language independently of specific systems to which the method applies. Proof scores for a specific system can be obtained by substituting the parameter modules of the parameterized modules with the specification modules of the specific system.
The effectiveness of the generic proof scores is demonstrated by applying them to two simple but non-trivial examples QLOCK and ABP.
http://www.jaist.ac.jp/~kokichi/talk/150226jaistVsemi/