Prof. Futatsugi's talk

It is our pleasure that Prof. Kokichi Futatsugi will talk about current trends in the verification of formal specifications with proof scores in CafeOBJ Algebraic Specification Language. The talk shall take place next Friday, November 9th, 12:00, at the Department of Mathematics of National Technical University of Athens.


=================================================
Title, Abstract, and Short Bio
=================================================

Title:

Verifying Specifications with Proof Scores in CafeOBJ
by Kokichi FUTATSUGI
Graduate School of Information Science
JAIST (Japan Advanced Institute of Science and Technology)
Nomi, Ishikawa, Japan

Abstract:

Verifying specifications is still one of the most important
undeveloped topics in software engineering. It is important because
quite a few critical bugs are caused at the level of domains,
requirements, and/or designs. It is also important for the cases where
no program codes are generated and specifications are analyzed/
verified only for justifying models of problems in real world. In
this talk, a survey of our research activities in verifying
specifications is given. After explaining fundamental issues and
importance of verifying specifications, the proof score approach in
CafeOBJ and its applications to several areas are described.


Short Bio of KF:

Kokichi Futatsugi is a professor of Graduate School of Information
Science, JAIST (Japan Advanced Institute of Science and Technology),
Ishikawa, Japan. His research interest includes formal methods,
software requirements and specifications, modeling and specification
languages. An important part of his research activities is done
around the CafeOBJ formal specification language
(www.ldl.jaist.ac.jp/cafeobj). CafeOBJ is an executable formal
specification language which has been designed and developed by an
international team headed by Prof. Futatsugi. He was a co-chair of
the program committee of the 20th International Conference on Software
Engineering (ICSE 1998) and an associate editor of ACM TOSEM
(Transaction of Software Engineering and Methodology) for 1995-2002.
He is a member of the advisory board of Journal of Higher-Order and
Symbolic Computation (www.wkap.nl/journals/hosc), and the editorial
board of Journal of Object Technology (www.jot.fm) and Journal of
Applied Logic (www.elsevier.com/locate/jal).
=================================================