Generic proof scores for the generate & check method in CafeOBJ


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/

Leave a comment

Your email address will not be published.