Specification and Verification with Proof Scores in CafeOBJ


Lecturer

FUTATSUGI, Kokichi
JAIST, Research Center for Software Verification, Japan

Place/Time

2015-10-23 and 10-30, NII, Tokyo, Japan.

Web site

Please see this page for details.

Abstract

CafeOBJ is a most advanced algebraic formal specification language system with rewriting/reduction engine which can be used for interactive verification. Proof scores are scripts for verifications and provide versatile ways to prove properties of specifications. The lectures give foundations and techniques of CafeOBJ/ProofScores by using elementary examples of natural numbers, lists, and a simple mutual exclusion protocol.

Leave a comment

Your email address will not be published.