Generic proof scores for the generate & check method in CafeOBJ

• Kokichi Futatsugi

Title: Generic proof scores for the generate & check method in CafeOBJ

Speaker: Kokichi Futatsugi (JAIST)

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.

https://www.jaist.ac.jp/~kokichi/talk/150226jaistVsemi/