Generate and check method for invariant verification in CafeOBJ

Prelegent(ci)

Kokichi Futatsugi

Afiliacja

JAIST-RCSV

Termin

9 września 2013 10:15

Pokój

p. 4070

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

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.

---