http://www.jaist.ac.jp/~kokichi/lecture/1611ICFEM/
Web Page for
Lecturers:
FUTATSUGI,Kokichi +
OGATA,Kazuhiro
( 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
tutorial give foundations and techniques of CafeOBJ/ProofScores by
using elementary examples of natural numbers, sequences, sets
and a simple mutual exclusion protocol.
Preliminary Material
Schedule and Material
- [Nov.15 (Tue) 10:00-11:00]
Proof Scores on Peano Style Natural Numbers
- [Nov.15 (Tue) 11:15-12:15]
Modeling, Specification, and Simulation of
Mutual Exclusion Protocol QLOCK
- [Nov.15 (Tue) 14:00-15:00]
Proof Score Development for QLOCK with Specification Calculus
- [Nov.15 (Tue) 15:15-16:15]
Formal Verification of Observational Transition Systems with Proof Scores
- [Nov.15 (Tue) 16:30-17:30]
Formal Verification of Observational Transition Systems with CafeOBJ CITP
Installation of the CafeOBJ Language System
Each attendee is expected to install CafeOBJ System version
1.5.5 (or later) to his/her own personal computer for executing examples
of the lectures. The specs and proof scores
of the lectures are prepared for the version 1.5.5
You can obtain CafeOBJ binaries for
Linux, MacOS, and Windows from the following web page.
CafeOBJ Web Page
http://www.jaist.ac.jp/~kokichi/lecture/1611ICFEM/