FORMES seminar, Fri, 03 Apr 2009 10:30

Title: Combining Inference and Search in Verification with CafeOBJ

Venue Tsinghua University, FIT Building, Room 1-515

Speaker Pr. Kokichi Futatsugi, Japan Advanced Institute of Science and

Technology. 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.