Make your programs run exactly as intended!
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 laboratoryHow 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
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  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 .
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 .
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
- A. Riesco, K. Ogata: Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. ACM TOSEM: (To appear)
- M. Zhang, K. Ogata: From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories. TCS 722: 52-75 (2018)
- A. Riesco, K. Ogata, K. Futatsugi: A Maude environment for CafeOBJ. FAoC. 29(2): 309-334 (2017)
Maude (a rewriting logic-based computer language and system)
CafeOBJ (an algebraic specification language and system)
For Master’s students: foundation is very crucial for good research; thus they are supposed to learn foundation, say through actively conducting course work; it would be better to decide their research topics mainly themselves but I would suggest some candidates among which they can choose.
For Doctoral students: they are supposed to be independent researchers or advanced engineers; thus it would be important to manage all necessary things mainly themselves and then they are treated as independent researchers.
For both: they are supposed to attend regular lab seminars, reporting on their research progress.