[ FUTATSUGI | IS | JAIST ]
JAIST IS
Lecture Web Page
Formal Methods (i613)
(Dec.8th, 2009 〜 Feb.9th, 2010・
TATSUNOKUCHI Campus）
Lectures： FUTATSUGI,Kokichi + OGATA,Kazuhiro
Teaching Assistant： ARIMOTO,Yasuhito
Supporters： NAKAMURA,Masahiro + GAINA,Daniel (+ CHIBA,Yuki)
(Send e-mail to
FUTATSUGI ＋ OGATA + ARIMOTO
for queries)
Contents of Lectures
(
Syllabus of lectures)
- Basics of CafeOBJ and Peano Style Natural Numbers (KF)
- Parameterized Modules and Generic List Structure (KF)
- Reasoning by Rewriting (MN)
- S&V (Specification and Verification) of Arithmetic Expression
Compiler (KO)
- Constructor Based Logic and Proof Score (DG)
- Modeling, Specification, and Verification of QLOCK
in OTS/CafeOBJ 1 (KF)
- Modeling, Specification, and Verification of QLOCK
in OTS/CafeOBJ 2 (KF)
- S&V of NSLPK 1 (KO)
- S&V of NSLPK 2 (KO)
- S&V of Graph Connectivity (DG)
- Combination of Inference and Search (in PS for QLOCK) (KF)
- S&V of Internal Control (YA)
- Collaborative Use of CafeOBJ and Maude (KO)
- Translation of OTS to Maude (MZ)
contents below will be updated frequently
Schedule and Materials (check frequently! schedule may change)
Assignment
Examination
You are allowed to bring in and refer to printed lecture notes
(incl. CafeOBJ code if you want), any books, and any conventional
documents (papers, manuals, etc.). However, you are not allowed to
bring in or use any computers.
Reference Materials
- CafeOBJ Home
Page: (manuals, systems, papers, etc)
-
CafeOBJ Report, -- The language, Proof Techniques, and Methodologies for
Object-Oriented Algebraic Specification --, by Razvan Diaconescu and Kokichi
Futatsugi, World Scientific, 1998, ISBN 981-02-3513-6.
-
CAFE: An Industrial-Strength Algebraic Formal Method, Edited by
Kokichi Futatsugi, etl al., Elsevier, 2000, ISBN 0 444 50556 3
-
Lecture Notes of Sinaia School on Formal Verification of Software
Systems
-
Introduction to CafeOBJ System (by SEINO,Takahiro)： Primary concise
introduction to CafeOBJ Language System
-
CafeOBJ入門 (清野貴博)： CafeOBJ言語システムの簡便な説明
- 日本ソフトウェア科学会のコンピュータソフトウェア誌に連載された『CafeOBJ入門』(全6回)
http://www.jaist.ac.jp/~kokichi/class/i613-0912/
[ Kokichi | IS | JAIST ]