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.

Kurzbiographie von Prof. Dr. Kokichi FUTATSUGI:

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 (<link www.ldl.jaist.ac.jp/cafeobj>www.ldl.jaist.ac.jp/cafeobj</link>). 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 SoftwareEngineering (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 (<link www.wkap.nl/journals/hosc>www.wkap.nl/journals/hosc</link>), and the editorial board of Journal of Object Technology (<link www.jot.fm>www.jot.fm</link>) and Journal of Applied Logic (<link www.elsevier.com/locate/jal>www.elsevier.com/locate/jal</link>).