Laboratory on Formal Methods and Trustworthy
School of Information
Advanced Institute of Science and Technology (JAIST)
- Current members
- Current projects
- Past members
- Past projects
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.
DOAN, Ha Thi Thu (from Hanoi, Vietnam)
HO, Tuan Dung (from HCM,
HA, Xuan Linh (from HCM,
NGUYEN, Tam Thi Thanh (from HCM, Vietnam)
PHAN, Huu Tho (from
Intern or rsearch students
(from China, graduated from Lanzhou Jiaotong
May Thu Aung
(from UIT, Myanmar)
DOAN, Ha Thi Thu: Model Checking Distributed Algorithms
HO, Tuan Dung: Machine Learning and Lemma Conjecture
SHIMOKAWA, Kensuke: TBD
NGUYEN, Tam Thi Thanh: Graphical Animations of State
HA, Xuan Linh: Program Development based on CafeOBJ
PHAN, Huu Tho: TBD
Projects conducted by
visiting fellows, intern students, etc.
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
A Study on Higly Reliable Formal Agile
Engineering Methods for Software Development, KAKEN 26240008, 2014-2018, PI:
PhD students and/or postdoc
ZHANG, Min (associate professor, East China Normal
CHAIMANONT, Thapana (Fujitsu, Ltd. --> Now in
APASUTHIRAT, Thanisorn (Fujitsu, Ltd.)
CHENG, Jian (NEC)
Intern or research
DAUDIER, Dorian (from ISAE-ENSMA,
MANDADI, Varuneshwar Reddy (Indian Institute of Science
Zakiah Binti Zulkefli (University of Science, Malaysia (Universiti
Sains Malaysia (USM))
VAN, Thi Hoai Phuong (VNU-HCM, University of
DASHZEWEG, Monhdelger (Mugi) (graduated from Department of
Accounting and Economy, Mandakh Burtgel University, Ulaanbaatar,
TRAIRATTANAPA, Vibhavee (Vee) (Chulalongkorn
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)
Study on Generating Efficient Rewrite Theory Specification from Behavioral
Specification, September 2011, by ZHANG, Min.
An Inverstigation on Machine Learning and
a Consideration on its Application to Theorem Proving, March 2016, by HO, Tuan
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
A Survey of Formal Verification of Paxos and a Case
Study with an Algebraic Specification Language, September 2014, by APASUTHIRAT,
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,
Projects conducted by visiting fellows, intern students,
Formal Verification of an Imperative Programming Language
Compiler, August 2016 - January 2017, by DAUDIER, Dorian.
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
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,
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,
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,
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.
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,
Development of Formal Specification Language for Writing
Specifications as Components Based on Functions, KAKEN 10558043, 1998-2001, PI:
A Study on Abstract Machines for Concurrent Rewriting,
KAKEN 07458056, 1995-1997, PI: FUTATUSGI, Kokichi
CITP in Maude
Feb 13, 2017 by ogata