Laboratory on Formal Methods and Trustworthy Software
30AUG2016.JPG - 133,501BYTES
(In front of YuuYuu (a restaurant near to JAIST) on Aug 30, 2016)
School of Information Science
Japan Advanced Institute of Science and Technology (JAIST)

- Outline
- Current members
- Current projects
- Past members
- Past projects
- Links

Formal mehods are one promising technology that could make software systems higly trustworthy. We have been studying formal methods, such as formal specification, intertactive theorem proving and model checking, tools supporting formal methods, and application of formal methods to software (and some other) systems. 

Current members

OGATA, Kazuhiro (professor)

PhD students

SHIMOKAWA, Kensuke (@tokyo)
DOAN, Thi Thu Ha (from Hanoi, Vietnam)
HO, Tuan Dung (from HCM, Vietnam)

Master students

HA, Xuan Linh (from HCM, Vietnam)
NGUYEN, Tam Thi Thanh (from HCM, Vietnam)
PHAN, Huu Tho (from HCM, Vietnam)
YANG, Zi (from China, graduated from Lanzhou Jiaotong University)

Intern or rsearch students

MANDADI, Manjukeshwar Reddy (from India, Amrita University)

Visiting fellows 

Current projects

PhD theses

DOAN, Thi Thu Ha: Model Checking Distributed Algorithms (tentative)
HO, Tuan Dung: Machine Learning and Lemma Conjecture (tentative)

Master Theses/Project Reports

NGUYEN, Tam Thi Thanh: Graphical Animations of State Machines
HA, Xuan Linh: Program Development based on CafeOBJ Specifications
PHAN, Huu Tho: An extendible and fast rewrite engine modulo associativity and commutativity (tentative)

Projects conducted by visiting fellows, intern students, etc.

Nothing particular now.


Principal investigator

Nothing particular now.


A Study on Higly Reliable Formal Agile Engineering Methods for Software Development, KAKEN 26240008, 2014-2018, PI: LIU, Shaoying.

Past members

PhD students and/or postdoc reseachers

ZHANG, Min (associate professor, East China Normal University)

Master students

ZHANG, Wenjie (Fujisoft Inc.)
CHAIMANONT, Thapana (Transtron (Thailand) Co.,Ltd. <-- Fujitsu, Ltd.)
APASUTHIRAT, Thanisorn (Fujitsu, Ltd.)

Intern or research students

DAUDIER, Dorian (from ISAE-ENSMA, France)
MANDADI, Varuneshwar Reddy (Indian Institute of Science (IISc))
Zakiah Binti Zulkefli (University of Science, Malaysia (Universiti Sains Malaysia (USM))
VAN, Thi Hoai Phuong (VNU-HCM, University of Technology)
DASHZEWEG, Monhdelger (Mugi) (graduated from Department of Accounting and Economy, Mandakh Burtgel University, Ulaanbaatar, Mongolia)
TRAIRATTANAPA, Vibhavee (Vee) (Chulalongkorn University)

Visiting fellows

May Thu Aung (lecturer, University of Information Technology, Myanmar)
RIESCO RODRIGUEZ, Adrian (assistant professor, Universidad Complutense de Madrid)
Kyawt Kyawt San (lecturer, University of Information Technology, Yangon, Myanmar)
CHOI, Yunja (associate professor, Kyungpook National University) 

Past projects (selected)

PhD theses

A Study on Generating Efficient Rewrite Theory Specification from Behavioral Specification, September 2011, by ZHANG, Min.

Master theses/project reports

An Inverstigation on Machine Learning and a Consideration on its Application to Theorem Proving, March 2016, by HO, Tuan Dung:.
Revisiting Model Checking of Chandy-Lamport Distributed Snapshot Algorithm, September 2015, by DOAN, Ha Thi Thu.
An Investigation of the Chandy-Lamport Distributed Snapshot Algorithm and its Model Checking, March 2015, by ZHANG, Wenjie.
A Survey of Allow Specification Language and Comparison with an Algebraic Specification Language, September 2014, by CHAIMANONT, Thapana.
A Survey of Formal Verification of Paxos and a Case Study with an Algebraic Specification Language, September 2014, by APASUTHIRAT, Thanisorn.
Description of an Invenory Management Problem in CafeOBJ and Assessment, March 2011, by SAKAMOTO, Atsushi.
Formalization of Anonymous Protocl Based on OTS/CafeOBJ Method, March 2008, by CHENG, Jian.

Projects conducted by visiting fellows, intern students, etc.

Formal Specification of PACE Protocol, June 2017, by MANDADI, Manjukeshwar Reddy
A Comparison of Two Clustering Algorithms by Applying them to Real-world Census Data, December 2016 - Feburary 2017, by May Thu Aung.
Model Checking Three Variants of Dijkstra Binary Semaphore with Maude and PAT, December 2016 - Feburary 2017, by May Thu Aung.
Formal Verification of an Imperative Programming Language Compiler, August 2016 - January 2017, by DAUDIER, Dorian.
A Proof Assistant and a Formal Proof Generator from Proof Scores on CafeInMaude, July 2016 - Augaust 2016, by RIESCO RODRIGUEZ, Adrian.
Formal Specification of PACE Protocol, May 2016 - June 2016, by MANDADI, Varuneshwar Reddy.
CafeInMaude: an Implementation of CafeOBJ in Maude, July 2015 - August 2015, by RIESCO RODRIGUEZ, Adrian.
Evaluation of Maude as a Test Generation Engine for Automotive Operating System, April 2013 - October 2013, by CHOI, Yunja.


Principal Investigator

A Study on Model Checking Distributed Algorithms whose Computational Targets are Distributed Systems, KAKEN 26540024, 2014-2016 .
Improvement of Liveness Model Checking Performace Degraded by Obese Formulas, KAKEN 23500041, 2011-2013.
Methodology and Environment for Effectively Using Theorem Provers and Model Checkers, KAKEN 18500019, 2006-2008.
A Study on Specification, Verification and Implementation of Reactive Systems, KAKEN 12780206, 2000-2001.
A Study on an Optimization Compiler for a Rewrite System, KAKEN 10780180, 1998-1999.


Development of an Innovative Specification Verification System based on Proof Score, KAKEN 23220002, 2011-2015, PI: FUTATSUGI, Kokichi.
Automating Security Analysis of E-Commerce Protocols, Asahi Glass Foundation, 2006-2009, PI: FUTATSUGI, Kokichi.
Safety Verification Technologies based on Behavioral Specifications, KAKEN 12133206, 2000-2003, PI: FUTATSUGI, Kokichi.
A Study on Coordination Models based on Module Systems, KAKEN 11878050, 1999-2001, PI: FUTATSUGI, Kokichi.
Development of Formal Specification Language for Writing Specifications as Components Based on Functions, KAKEN 10558043, 1998-2001, PI: FUTATSUGI, Kokichi.
A Study on Abstract Machines for Concurrent Rewriting, KAKEN 07458056, 1995-1997, PI: FUTATUSGI, Kokichi


CITP in Maude
K Framework
Joseph Goguen
Leslie Lamport

Jun 5, 2017 by ogata