Institute of Computer Languages
Compilers and Languages Group
über
| Datum: | Montag, 7. März 2011 |
|---|---|
| Zeit: | 14:00 c.t. |
| Ort: | TU Wien, Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte) |
One of the most important technical issues in current system verification is how to combine inference (a la interactive theorem proving) and search (a la automatic model checking) in an effective and efficient way.
CafeOBJ is a most advanced algebraic formal specification language system with rewriting/reduction engine which can be used for interactive verification. CafeOBJ also has a searching facility which can be used to search all reachable states of a system to check whether some property holds for all reachable states. We have been developing an interactive verification method with proof scores in CafeOBJ, and are currently trying to combine this method with the searching to achieve more powerful verification method.
In this talk, our current achievement of combining inference and search in verification is explained by using a simple but non-trivial example of mutual exclusion protocol.
Kokichi Futatsugi has been a professor of JAIST since 1993. Before
getting a full professorship at JAIST, he worked at ETL
(Electrotechnical Laboratory), MITI (Ministry of International Trade
and Industry), Japanese Government and was appointed the Chief
Researcher of ETL in 1992. He worked also at SRI International
(Stanford Research Institute), California for 1983-1984 as a visiting
researcher. His research interests include formal specification
languages, formal methods, systems verifications, software
requirements/specifications, and his current research activities are
centered around formal specification and verification based on CafeOBJ
(an executable formal specification language). He got a Fellow Award
of Japan Society for Software Science and Technology in 2008, and is
now adviser/editor of international journals like IJSI (www.ijsi.org),
JAL (www.elsevier.com/locate/jal), and JHOSC
(www.springerlink.com/content/102420/).
(http://www.jaist.ac.jp/~kokichi/)
Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.