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)
Researchers
PREINING, Norbert (Accelia,inc.)
PhD
students
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)
DO, Minh Canh (from VNU-UET) (DRF Special; Supported by NEC C&C
to attend SEKE 2019; Supported by The Telecommunication Advancement Foundation
to attend APSEC 2020)
BUI, Duy Dang (from VNU-HCM)
(DRF Normal; NEC C&C Grants for non-Japanese Reseachers 2021)
TRAN, Dinh Duong (from VNU-UET) (DRF Normal; NEC C&C Grants
for non-Japanese Reseachers 2022; Supported by NEC C&C to attend SEKE
2021)
Thet Wai Mon (from UIT, Myanmar) (DRF
Special)
TAKAGI, Tsubasa (from Tojo lab) (SD; JSPS DC1)
Master
students
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)
Intern or
rsearch
students
...
Visiting
fellows
...
Current
projects
PhD
theses
Yati Phyo : A divide & conquer approach to LTL model
checking
DO, Minh Canh : A scalable testing
technique for concurrent programs
BUI, Duy Dang : A
systematic way to conjecture lemmas for formal systems verification based on
state machine visual information
TRAN, Dinh Duong :
Formal verification and analysis of post-quantum cryptographic
protocols
Thet Wai Mon : Graphica animations of
post-quantum cryptographic protocols for formal verification
TAKAGI, Tsubasa
: Logics for quantum computintg
Master
Theses/Project Reports
LIU, Minxuan : Formal
specification and model checking of a merging control protocol for self-driving
vehicles in Maude
OGURA, Tomoyoshi : An investgation of formal verification
of distributed concensus protocols
ISHIBASHI, Takanori : Model checking the
distributed consensus protocol Raft
NAKAMURA, Tsuyoshi : TBD
WAKI, Kentaro
: TBD
OSAWA, Hiroaki : TBD
Moe Nandi Aung : A divide & conquer
approach to eventual mode checking
Projects
conducted by visiting fellows, intern students,
etc.
...
Grant-in-aid
Principal
investigator
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
...
Past
members
PhD students
and/or postdoc reseachers
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
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
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
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
Graphical animations of
authentication protocols by Thet Wai Mon
An investigation of the proof score
approach to formal verification & its case studies and a new case study with
the approach by ASAE, Naoki
An investigation of formal verification of
authentication protocols with proof score and a new case study, March 2021,
FUJII, Shuho
An investigation of improvement of liveness model checking
performance degraded by obese formulas, March 2021, KOYANAGI, Satoshi
An
investigation of a state machine visualization tool SMGA & case studies with
SMGA, March 2021, KOBAYASHI, Midori
Formal verification of some mutual
exclusion protocols with CafeInMaude, its proof
assistant and its proof generator, September 2020, 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 Ekerfs 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.
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
Jan 27, 2022; March 29, 2021; Jan 13, 2021; Jun 1, 2020 by ogata