Laboratory on Formal Methods and Trustworthy Software

(In front of YuuYuu (a restaurant near 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

Outline
.
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)
DO, Minh Canh (assistant professor)

Researchers

PREINING, Norbert (Accelia,inc.)

PhD students

ISHIBASHI, Takanor (@tokyo))

Master students

KONDO, Yohei (@tokyo)
MATSUURA, Takahiro (@tokyo)
MAGOME, Kyosuke (@tokyo)
KONG, Fanyi
HO, Tan Hoang (from LQDTU) (1+1 program student)
U, Cao Ky Long (from University of Science, VNU-HCM) (1+1 program student)
NGUYEN, Thu Phuong (from LQDTU) (1+1 program student) whose main supervisor is Canh Minh Do
PHAM, Quoc Vuong (from University of Science, VNU-HCM) (1+1 program student) whose main supervisor is Canh Minh Do

Intern or rsearch students
...

Visiting fellows 

...

Current projects

PhD theses

ISHIBASHI, Takanori: ...


Master Theses/Project Reports

KONDO, Yohei (@tokyo): ...
MATSUURA, Takahiro (@tokyo): ...
MAGOME, Kyosuke (@tokyo): ...
KONG, Fanyi: ...
HO, Tan Hoang: ...
U, Cao Ky Long: ...

Projects conducted by visiting fellows, intern students, etc.

...

Grant-in-aid

Principal investigator

Logical foundation and formal verification of quantum-resistant security protocols, KAKEN 24KK0185, 2024-09-09 - 2028-03-31

Co-investigator

Development of model checking techniques for enabling dependable distributed systems, KAKEN 23K28060, 2023-04-01 - 2027-03-31

Past members

PhD students and/or postdoc reseachers

TAKAGI, Tsubasa (associate professor of JAIST) (from Tojo lab) (SD; JSPS DC1)
TRAN, Dinh Duong (assistant professor of JAIST) (from VNU-UET) (DRF Normal; NEC C&C Grants for non-Japanese Reseachers 2022; Supported by NEC C&C to attend SEKE 2021)
BUI, Duy Dang (lecturer of University of Science, VNU-HCM) (from VNU-HCM) (DRF Normal; NEC C&C Grants for non-Japanese Reseachers 2021)
DO, Minh Canh (assitant professor of JAIST) (from VNU-UET) (DRF Special; Supported by NEC C&C to attend SEKE 2019; Supported by The Telecommunication Advancement Foundation to attend APSEC 2020
Yati Phyo (from UIT, Myanmar) (DRF Normal; NEC C&C Grants for non-Japanese Reseachers 2020; Iuchi Asia Students Scholarship 2021; Supported by NEC C&C to attend COMPSAC 2021)
Thet Wai Mon (from UIT, Myanmar) (DRF Special)
DOAN, Thi Thu Ha (postdoc reseacher at Freiburg University (Germany)) DBLP Google Scholar (Supported by NEC C&C to attend ICDCS 2017)
ZHANG, Min (associate professor, East China Normal University) DBLP Google Scholar
HO, Tuan Dung (moved to Dam lab in School of Information Science)
SHIMOKAWA, Kensuke

Master students

HOAN, Trong Binh (from LQDTU)
LIU, Minxuan
OGURA, Tomoyoshi (@tokyo)
ISHIBASHI, Takanori (@tokyo)
NAKAMURA, Tsuyoshi (@tokyo)
WAKI, Kentaro (@tokyo)
OSAWA, Hiroaki (@tokyo)
Moe Nandi Aung (from UIT, Myanmar) (MEXT Scholarship)
ASAE, Naoki (Hitachi)
KOBAYASHI, Midori (Toppan)
FUJII, Shuho (Panasonic)
KOYANAGI, Satoshi (@tokyo)
ZI, Yang (the information center in LanZhou university 1st hospital,)
MOHAMMAD, Farhan Ferdous (ONODANI co.,ltd.)
NGUYEN, Tam Thi Thanh (Supported by NEC C&C to attend DASC 2017)
PHAN, Huu Tho (MIS)
HA, Xuan Linh (a reseacher in NUS)
HO, Tuan Dung (Dam lab in School of Information Science)
ZHANG, Wenjie (Fujisoft Inc.)
CHAIMANONT, Thapana (Transtron (Thailand) Co.,Ltd. <-- Fujitsu, Ltd.)
APASUTHIRAT, Thanisorn (Fujitsu, Ltd.)
SAKAMOTO, Atsushi
CHENG, Jian (NEC)

Intern or research students

TRINH, Thi Thu Huyen (from Electornic Power University, Hanoi, Vietnam
DOAN, Vu Thuan (from VNU-HCM)
KUMAR, Abhay (from Ramaiah Institute of Technology, Visvesvaraya Technological University)

Moe Nadi Aung (from UIT, Myanmar) (2nd time visit and stay as an internship student)
Khin Me Me Lattt (From UIT, Myanmar)
YAN, Zhenzhu (from Hokuriku U.)

XIONG, Ye (from Hokuriku U.)

LIU, Minxuan (from Hokuriku U.)

GUPTA, Parth (from IIT Kharagpur).
BUI, Xuan Thuy (from Le Quy Don Technical University, Vietnam)
Moe Nadi Aung (from UIT, Myanmar)
Myat Theingi Kyaw (from UIT, Myanmar)
Htet Htet Wai (from UIT, Myanmar)
MANDADI, Manjukeshwar Reddy (from India, Amrita University)
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 (associate professor, University of Information Technology, Myanmar)
RIESCO RODRIGUEZ, Adrian (associate 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

Quantum Dynamic Algebra: From Orthomodular Lattice to Algebra of Quantum Programs, September 2023, by TAKAGI, Tsubasa
Formal verification with algebraic techniques and its application, September 2023, by TRAN, Dinh Duong
State Machine Visualization Based on Gestalt Principles and Its Applications, December 2022, by BUI, Duy Dang
State Machine Visualization Based on Gestalt Principles and Its Applications, September 2022, by DO, Minh Canh
A Divide & Conquer Approach to Leads-to and Conditional Stable Model Checking, September 2022, by Yati Phyo
Formal Specification and Model Checking of Distributed Systems with Rewriting Logic-based Meta-programming Facilities, March 2019, by DOAN, Ha Thi Thu
A Study on Generating Efficient Rewrite Theory Specification from Behavioral Specification, September 2011, by ZHANG, Min.

Master theses/project reports

Formal specification and analysis of Post-quantum OpenPGP protocol in CafeOBJ, September 2025, by HOAN, Trong Binh
Formal Specification and Model Checking of Distributed Leader Election Protocols [Project Report], March 2024, by OGURA, Tomoyoshi
Formal specification and model checking studies using Maude [Project Report], March 2024, by NAKAMURA, Tsuyoshi
Investigation and Visualization of K Framework [Project Report], March 2025, by OSAWA, Hiroaki
Formal specification and model checking of a recoverable wait-free version of MCS, Decemver 2024, by WAKI, Kentaro
Formal Specification and Model Checking of the Distributed Consensus Protocol Raft, September 2023, by ISHIBASHI, Takanori
A Technique to Alleviate the State Space Explosion for Eventual Model Checking, Its Support Tool and Case Studies, September 2023, by Moe Nandi Aung
Formal specification, model checking and graphical animation of an autonomous vehicle merging protocol [Project Report], March 2022, by LIU, Minxuan
An investigation of the proof score approach to formal verification and a new case study with the approach [Project Report], September 2021, by ASAE, Naoki
An investigation of a state machine visualization tool SMGA & case studies with SMGA [Project Paper], March 2021, by KOBAYASHI, Midori
An investigation of formal verification of authentication protocols with proof score and a new case study [Project Paper], March 2021, by FUJII, Shuho
An investigation of improvement of liveness model checking performance degraded by obese formulas [Project Paper], March 2021, by KOYANAGI, Satoshi
Graphical animations of authentication protocols, September 2021, by Thet Wai Mon
Formal verification of some mutual exclusion protocols with CafeInMaude, its proof assistant and its proof generator, September 2020, by TRAN, Dinh Duong
A Divide & Conquer Approach to Leads-to Model Checking, September 2019, by Yati Phyo

An Environment for Testing Concurrent Programs Based on Rewrite-theory Specifications, September 2019, by DO, Minh Canh

A Study on Application of State Machine Graphical Animation to Distributed Protocols, September 2019, by BUI, Duy Dang

Investigation and Specification of Path Finding Algorithms, March 2019, by ZI, Yang
An investigation of applications of state machines, September 2018, by MOHAMMAD, Farhan Ferdous
An Investigation of the Steven Eker’s Approach to Associative-Commutative Matching, March 2018, PHAN, Huu Tho
Graphical Animations of State Machines, September 2017, by NGUYEN, Tam Thi Thanh
Program development in Java based on CafeOBJ specifications, September 2017, by HA, Xuan Linh
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 and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol, October 2018 - December 2018, by Moe Nadi Aung
Proof Repair, July 2018 - August 2018, by RIESCO, Adrian
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.

Grant-in-aid

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.
Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, JST SICORP Grant Number JPMJSC20C2, Japan, April 2021 - March 2024
Visualization of Security Proocols, FY2020 grant-in-aid for new technology research activities at universities (SHIBUYA SCIENCE CULTURE AND SPORTS FOUNDATION)
A divide and conquer approach to parallelization of LTL model checking, KAKEN 19H04082, April 2019 - March 2022

Co-investigator

A Study on Higly Reliable Formal Agile Engineering Methods for Software Development, KAKEN 26240008, 2014-2018, PI: LIU, Shaoying.
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

Links

CafeOBJ
Maude
SAL
PAT
Coq
Event-B
CITP in Maude
K Framework
COMPCERT
Joseph Goguen
Leslie Lamport

Dec 15, 2025; Jan 27, 2022; March 29, 2021; Jan 13, 2021; Jun 1, 2020 by ogata