JAIST-FSSV2010 Lecture Materials

Some lecture materials posted in this page will be renewed at the very last moment, even after starting the school, and it is recommended to check this page frequently.

You can download the whole contents of this page from here (.zip file).

Lecture 01: Basics of CafeOBJ and Peano Style Natural Numbers

Lecture 02: Parametrized Modules and Generic List Structure

Lecture 03: Models and Proof Rules for Proof Scores in CafeOBJ

Lecture 03a: An overview of Models and Proof Rules

Lecture 03b: Constructor-based Institutions

Lecture 04: Inference with Rewriting Rules

Lecture 05: Modeling, Specification, and Verification of Mutual Exclusion Protocol (QLOCK) in OTS/CafeOBJ

Lecture 05a: Modeling and Specification of QLOCK in OTS/CafeOBJ

Lecture 05b: Proof Score Writing for QLOCK in OTS/CafeOBJ

Lecture 06: Modeling and Specification of Authentication Protocol (NSLPK) in OTS/CafeOBJ

Lecture 07: Verification of NSLPK and Some Tips for Construction of Proof Score

Lecture 08: Stainless Formal Verification

Lecture 09: Combination of Inference and Search in Verification with Proof Score

Lecture 09a: Combining Inference and Search in QLOCK Verification

Lecture 09b: A Collaborative Use of CafeOBJ and Maude

Lecture 10: An Introduction to Maude

Lecture 11: The Maude Formal Tool Environment

Lecture 12: Model Checking Verification in Maude

Back
last update: 2010.03.30