[ FUTATSUGI | IS | JAIST ]
Web Page for Lectures/Labs on
Specification and Verification with Proof Scores in CafeOBJ
at DTU, 21-22 June 2010
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/labs give foundations and techniques of CafeOBJ/ProofScores by
using elementary examples of natural numbers, lists, and a simple
mutual exclusion protocol.
Schedule
21 June 2010 (Monday)
09:00 - 10:30 Lecture 1
10:45 - 12:00 Lab 1
12:00 - 13:00 Lunch
13:00 - 14:30 Lecture 2
14:45 - 16:00 Lab 2
22 June 2010 (Tuesday)
09:00 - 10:30 Lecture 3
10:45 - 12:00 Lab 3
12:00 - 13:00 Lunch
13:00 - 14:30 Lecture 4
14:45 - 16:00 Lab 4
Lectures/Labs Materials
(Please notice that contents of the following meterials may be changed.)
Preparation:
-
Every student is supposed to do the following
before attending the Lectures/Labs.
- Install to her/his personal computer CafeOBJ system
from the following web page.
- Study the contents of the following web page.
-
Every student is recommended to look into the following slides.
Lecture/Lab 1: Basics of CafeOBJ and Peano Style Natural Numbers
Lecture/Lab 2: Parametrized Modules and Generic List Structure
Lecture/Lab 3: Modeling and Specification of
Mutual Exclusion Protocol (QLOCK) in OTS/CafeOBJ
Lecture/Lab 4: Proof Score Writing for QLOCK in OTS/CafeOBJ
Related Web Pages
http://www.jaist.ac.jp/~kokichi/seminar/dtu1006/
[ Kokichi | IS | JAIST ]
last update: 2010.6.22