Lecturers: FUTATSUGI,Kokichi ,  OGATA,Kazuhiro,  NAKAMURA,Masaki
Teaching Assistant :  GAINA, Daniel
         JAIST (Japan Advanced Institute of Science and Technology)

Materials for the lectures [slides (pdf files) and CafeOBJ codes (text files with .mod extension)] :

• Introductory Talk Slides: Verifying Specifications with Proof Scores in CafeOBJ
• Lecture 1 Slides: Basics Modeling, Specification, Verification
  
• natPlus.mod
• basicNatPlus.mod
• natPlusAssocPS.mod
• nat+.mod
• ratDiv.mod
• =and==.mod
• nat+ps.mod
• constVsVar.mod
• Lecture ２ Slides:  Models and Structuring of Specifications
  
• structSpecSTG.mod
• stringOfString.mod
• Exercise 1 Slides: Basic Exercises on CafeOBJ
  
• commands.mod
• red.mod
• comments.mod
• nat+.mod
• nat+err.mod
  
• stack.mod
• Lecture 3 Slides: Reasoning by Rewriting
• trs.mod
• termination.mod
• confluence.mod
• conditional.mod
• ac.mod
  
• Lecture 4 Slides: Verification by Induction
• proofscore.mod
• leftid.mod
• comm.mod
• concat.mod
• reverse.mod
  
• Exercise 2 Slides
  
• exercise02.mod
  
• Lecture 5 Slides: Modeling and Specification in  OTS/CafeOBJ
• qlock.mod
• invariants-0.mod
  
• Lecture 6 Slides: Verification with Proof Score
• qlock Proof Score
• Exercise 3
  
• Lecture 7 Slides:  Analysis of Alternating Bit Protocol 1
  
• ABP Proof Score
  
• Lecture 8 Slides: Analysis of Alternating Bit Protocol  2
• Exercise 4 Slides: Analysis of Simple Communication Protocol 1
• scp.mod
  
• Lecture 9  Slides:  Analysis of Simple Communication Protocol  2
• scp.mod
• experiment.mod
• invariants.mod
• template.mod
• proof1.mod
• proof2.mod
• proof3.mod
• proof4.mod
• proof5.mod
• verify.mod
  
• Lecture 10 Slides: Falsification and Verification by Searching
  
• searchCommand.mod
• readerWriter.mod
• qlockWithSepWant.mod
• qlockWithSepWantFalsify.mod
• Exercise 5
  

Related web pages:

•  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

Supposed preliminary knowledge: 

• fundamental knowledge on programming, algorithm, data structure, automaton & formal language, and mathimatical logic

E-mail for questions and submitting answers for examination:

• toTheLecturesAndTA
  

• problems (in text  file)