http://www.jaist.ac.jp/~kokichi/lecture/1609NII/

---

Web Page for the Course of Lectures:

Introduction to Specification Verification with CafeOBJ

on 16(Fri,13:30-17:00) + 23(Fri,13:30-17:00) September 2016
at NII, Tokyo, Japan

Lecturer:   FUTATSUGI,Kokichi ( JAIST)
      (Send e-mail to FUTATSUGI "futatsugi at jaist.ac.jp" for queries)

---

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, sequences, sets and a simple mutual exclusion protocol.
    A new topic of this year's course is "automation of case analyses with Specification Calculus" that helps to achieve non-trivial interactive verifications systematically.

---

Goal of the Course

    To obtain the following abilities by solving several simple but non-trivial examples with CafeOBJ Language System. (1) formalizing domain, requirement, design specifications based on the formal systems like sets, functions/maps, algebras. (2) analysing and/or verifying the obtained formal specifications.

---

Preliminary Materials:

• Web page of a brief introduction to CafeOBJ System (in English)
• Web page of a brief introduction to CafeOBJ System (in Japanese)
• A Brief Overview of CafeOBJ/ProofScore and Formal Methods

---

Lecture Schedule and Materials

1. [Sep.16 (Fri) 13:30-15:00]  Basics of CafeOBJ and Peano Style Natural Numbers
   
   Material for Lecture 1
2. [Sep.16 (Fri) 15:15-16:45]  List, Seq, Set and Specification Calculus
   
   Material for Lecture 2
3. [Sep.16 (Fri) 16:45-17:00]  Questions and Answers
   


4. [Sep.23 (Fri) 13:30-15:00]  Modeling, Specification, and Simulation of Mutual Exclusion Protocol QLOCK
   
   Material for Lecture 3
5. [Sep.23 (Fri) 15:15-16:45]  Proof Score Development for QLOCK with Specification Calculus
   
   Material for Lecture 4
6. [Sep.23 (Fri) 16:45-17:00]  Questions and Answers
   

---

Installation of 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, exercises, and assignments 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.

http://cafeobj.org/download/

---

CafeOBJ Web Page

CafeOBJ Official Web Page

---

http://www.jaist.ac.jp/~kokichi/lecture/1609NII/