Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Aktualności — Wydarzenia

SLIWOWICA

 

Generate and check method for invariant verification in CafeOBJ


Seminarium Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji (SLIWOWICA)

Prelegent: Kokichi Futatsugi

2013-09-09 10:15

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.