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.