Introduction to Specification and Verification in CafeOBJ

  • 2012-07-18
  • Research

The lectures gradually develop executable algebraic semantics (or specifications) of a simple imperative programming language called Minila


After introductory explanations of the CafeOBJ algebraic specification language system, the lectures gradually develop executable algebraic semantics (or specifications) of a simple imperative programming language called Minila. The semantics/specifications are composed of that of an interpreter of Minila, an abstract machine, and a compiler from Minila to machine codes of the abstract machine. A verification of a part of the compiler is also given.

The lectures are prepared for the beginners for CafeOBJ and only fundamental knowledge of algorithms and data structures, automata and languages, elementary mathematical logic are assumed. The lectures are also designed to be combined with interactive exercises with the CafeOBJ language system, and all attendees are expected to bring in their personal computers to class room. After attending the lectures, the attendees are expected to be able to construct elementary formal semantics/specifications in CafeOBJ and write proof scores for verifying properties about the semantics/specifications.


Kokichi Futatsugi has been a professor of JAIST since 1993. Before getting a full professorship at JAIST, he worked at ETL (Electrotechnical Laboratory), MITI (Ministry of International Trade and Industry), Japanese Government and was appointed the Chief Researcher of ETL in 1992. He worked also at SRI International (Stanford Research Institute), California for 1983-1984 as a visiting researcher. His research interests include formal specification languages, formal methods, systems verifications, software requirements/specifications, and his current research activities are centered around formal specification and verification based on CafeOBJ (an executable formal specification language). He got a Fellow Award of Japan Society for Software Science and Technology in 2008, and is now adviser/editor of international journals like IJSI, JAL, and JHOSC.


Wednesday, July 18, 2012 Basics of CafeOBJ and Peano Style Natural Numbers

Lecture: 10:00-11:30 Exercise: 14:00-15:30

Wednesday, July 25, 2012 Parametrized Modules and Generic List Structure

Lecture: 10:00-11:30 Exercise: 14:00-15:30

Wednesday, August 1, 2012 Definition of Minila Programming Language and Its Interpreter and Virtual Machine

Lecture: 10:00-11:30 Exercise: 14:00-15:30

Wednesday, August 8, 2012 Compiler of Minila and Its Verification with Proof Scores

Lecture: 10:00-11:30 Exercise: 14:00-15:30


This lecture and tutorial series is organized by the Compilers and Languages Group at the Institute of Computer Languages.


Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!