Web Page for Introductory Lectures on
Specification and Verification
with Proof Scores in CafeOBJ
at NII, Tokyo
on 23+30 October 2015
by
FUTATSUGI,Kokichi
( JAIST )
Overview
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.
Schedule
23 October 2015 (Friday)
13:30 - 15:00 Lecture 1
15:15 - 16:45 Lecture 2
30 October 2015 (Friday)
13:30 - 15:00 Lecture 3
15:15 - 16:45 Lecture 4
Lectures Materials
(Please notice that contents of the following meterials
may change until the end of the lectures.)
Lecture 1: Basics of CafeOBJ and Peano Style Natural Numbers
Lecture 2: Parametrized Modules and Generic List Structure
Lecture 3: Modeling, Specification, and Simulation of
Mutual Exclusion Protocol (QLOCK) in CafeOBJ
Lecture 4: Proof Score Writing for QLOCK
with Generate & Check Method
in CafeOBJ
Related Web Pages
http://www.jaist.ac.jp/~kokichi/lecture/1510NII/
[ FUTATSUGI,Kokichi ]
Update dates: 2015.10.28