Past projects (selected)
A Study on Generating Efficient Rewrite Theory Specification from Behavioral Specification, September 2011, by ZHANG, Min.
Master theses/project reports
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 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.
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