Generate and check method for invariant verification in CafeOBJ

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.