Generate and check method for invariant verification in CafeOBJ

Speaker(s)

Kokichi Futatsugi

Affiliation

JAIST-RCSV

Date

Sept. 9, 2013, 10:15 a.m.

Room

room 4070

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

Effective coordination of inference (a la theorem proving) and search (a la model checking) is one of the most important and interesting research topics in formal methods.  We have developed several kinds of techniques for coordinating inference and search.
The generate and check method is a recent development for invariant verification with proof scores in CafeOBJ.  The method is based on (1) state representations as sets of observers, and (2) systematic generation of finite state patterns which cover all possible states.

---