Make your programs run exactly as intended!

OGATA Laboratory
Professor：OGATA Kazuhiro

E-mail：
［Research areas］
Formal methods
［Keywords］
formal specification, model checking, theorem proving, distributed systems, state machine graphical animation

Skills and background we are looking for in prospective students

No matter what academic subjects they have taken, they have done their BEST to tackle them and no matter what difficulties they will encounter, they are supposed to keep highly motivated.

What you can expect to learn in this laboratory

How to formalize distributed (distributed) systems as state machines.
How to describe state machines in a formal specification language, such as Maude and CafeOBJ.
How to formally verify (e.g. theorem prove and model check) that state machines enjoy desired properties

【Job category of graduates】Researcher, Engineer

Research outline

Many system failures caused by software systems have been broadcasted. This implies that humans have not known how to create programs that can run exactly as intended. One possible promising way to do so is to use theorem proving. Our intentions can be described as desired properties and software systems can be formalized as state machines.

Desired properties as well as state machines can be described as formal specifications in formal specification languages, such as Maude and CafeOBJ. We could mechanically prove that state machines enjoy desired properties based on formal specifications. In this category of research, the second implementation of CafeOBJ called CafeInMaude has been developed on top of Maude [3] and a proof assistant called CiMPA and a proof generator called CiMPG, which automatically generates proof scripts for CiMPA from proof scores in CafeOBJ, have been developed [1].

Model checking is another promising formal verification technique. It is necessary to prepare different formal specifications for model checking than those for theorem proving. A way to transform the former from the latter has been invented [2].

Theorem proving often needs many lemmas. It is necessary to understand state machines well to conjecture good lemmas. A state machine graphical animation tool called SMAG has been developed for this purpose (See Figure 1).

Figure 1. A picture generated by SMGA

Key publications

1. A. Riesco, K. Ogata: Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. ACM TOSEM: (To appear)
2. M. Zhang, K. Ogata: From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories. TCS 722: 52-75 (2018)
3. A. Riesco, K. Ogata, K. Futatsugi: A Maude environment for CafeOBJ. FAoC. 29(2): 309-334 (2017)

Equipment

Maude (a rewriting logic-based computer language and system)
CafeOBJ (an algebraic specification language and system)