Institute of Computer Languages
Compilers and Languages Group
on
| Date: | Wednesday, March 12th, 2008 |
|---|---|
| Time: | 14:00 (s.t.) |
| Location: | TU Wien, Elektrotechnik, EI 1 Petritsch-Hörsaal, Gußhausstraße 25-29 (Altbau), 2. Stock |
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.
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).