Desktop Site

News & Events


Advanced School on Formal Specification and Systems Verification 2010 will be held on March 1-5, 2010.

・ March 1st-5th, 2010
JAIST, Nomi, Ishikawa, Japan  and  Kanazawa Excel Hotel Tokyu, Kanazawa, Ishikawa, Japan


JAIST (Japan Advanced Institute of Science and Technology) has provided an advanced school which is designed to give a series of lectures on recent activities about formal specification and systems verification with CafeOBJ and Maude. CafeOBJ and Maude are sister languages of OBJ language, and two of the most advanced formal specification languages for systems verification.

This was the first JAIST advanced school on this subject and lectures of the school covered the following topics:

  • Modeling and Specification in Order-Sorted Algebras
  • Modeling and Specification in Observational Transition Systems (OTS)
  • Modeling and Specification in Rewriting Rules (RRL)
  • Interactive verification with proof score methodology in CafeOBJ
  • Automatic verification with sophisticated search methodology in Maude
  • Combination of inference (a la interactive theorem proving) and search (a la automatic model checking) in verifications with the coherent CafeOBJ/Maude framework