Institute of Computer Languages
Compilers and Languages Group

Talks 2004 - Kokichi Futatsugi

The Database and Artificial Intelligence Group and the Compilers and Languages Group invite you to a talk given by

Prof. Dr. Kokichi Futatsugi

(JAIST - Japan Advanced Institute of Science and Technology, Ishikawa, Japan) on

Equational Proofs in CafeOBJ

Date: Thursday, September 2, 2004
Time: 16:15
Location: TU Wien, building at the Freihaus, FH HS 4, Wiedner Hauptstraße 8, Turm B, yellow area, 2nd upper floor

Abstract:

CafeOBJ is a formal specification language equipped with verification methodologies based on algebraic specification techniques. It is also the first algebraic specification language which incorporates observational (or behavioral) specifications based on coherent hidden algebras. Observational specifications in CafeOBJ can be seen as a nice combination of static and dynamic specifications, and facilitate natural and transparent specification and verification of complex systems.

This talk explains an interactive equational proof method in CafeOBJ. Ways to write proof score in CafeOBJ is analyzed based on several case studies of verifying distributed mutual exclusion algorithms and security protocols. This analysis leads to a method to divide a formula stating a property under inductive proof into small ones, each of which is proved by writing proof scores independently. It is argued that this can relieve the load to reduce logical formulas and decrease the number of subcases into which the case is split in case analysis.

The talk also mentions some practical applications of this method.

About Prof. Dr. Kokichi Futatsugi:

Professor Futatsugi assumed a concurrent position at JAIST in April 1992 while he was working mainly for ETL (Electrotechnical Lab.) as Chief Senior Researcher. In April 1993, he starts to work mainly for JAIST. He received the Ph.D. degree from Tohoku University, and joined ETL in 1975. Professor Futatsugi stayed at SRI International as an International Fellow for one year from 1983 to 1984.
Complang
   About Us
   Research
   Lehre
   Service
      Robotics
      Library
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Sitemap
Contact
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)