Argument Filtering Transformation. - Keiichirou Kusakari; Masaki Nakamura 001; Yoshihito Toyama (PPDP, 1999)

The evaluation strategy for head normal form with and without on-demand flags. - Masaki Nakamura 001; Kazuhiro Ogata 001 (WRLA, 2000)

Chocolat/SMV: A Translator from CafeOBJ into SMV. - Kazuhiro Ogata 001; Masahiro Nakano; Masaki Nakamura 001; Kokichi Futatsugi (PDCAT, 2005)

Automating Invariant Verification of Behavioral Specifications. - Masahiro Nakano; Kazuhiro Ogata 001; Masaki Nakamura 001; Kokichi Futatsugi (QSIC, 2006)

A Behavioral Specification of Imperative Programming Languages. - Masaki Nakamura 001; Masahiro Watanabe; Kokichi Futatsugi (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2006)

Elimination Transformations for Associative-Commutative Rewriting Systems. - Keiichirou Kusakari; Masaki Nakamura 001; Yoshihito Toyama (J. Autom. Reason., 2006)

On Equality Predicates in Algebraic Specification Languages. - Masaki Nakamura 001; Kokichi Futatsugi (ICTAC, 2007)

CrÈme: an Automatic Invariant Prover of Behavioral Specifications. - Masahiro Nakano; Kazuhiro Ogata 001; Masaki Nakamura 001; Kokichi Futatsugi (Int. J. Softw. Eng. Knowl. Eng., 2007)

A Specification Translation from Behavioral Specifications to Rewrite Specifications. - Masaki Nakamura 001; Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Inf. Syst., 2008)

User-Defined On-Demand Matching. - Masaki Nakamura 001; Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Inf. Syst., 2009)

Generating Test Cases for Invariant Properties from Proof Scores in the OTS/CafeOBJ Method. - Masaki Nakamura 001; Takahiro Seino (IEICE Trans. Inf. Syst., 2009)

Specification Translation of State Machines from Equational Theories into Rewrite Theories. - Min Zhang 002; Kazuhiro Ogata 001; Masaki Nakamura 001 (ICFEM, 2010)

Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications. - Masaki Nakamura 001; Kazuhiro Ogata 001; Kokichi Futatsugi (J. Symb. Comput., 2010)

Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support. - Min Zhang 002; Kazuhiro Ogata 001; Masaki Nakamura 001 (IEICE Trans. Inf. Syst., 2011)

Preliminary results of pointing and calling detection system for nurses. - Akira Urashima; Masaki Nakamura 001; Tomoji Toriyama; Junichi Oshima; Mitsuko Nakagawa; Tadao Nomura (APCHI, 2013)

To parallelize or not to parallelize, bugs issue. - Alaa I. El-Nashar; Masaki Nakamura 001 (CoRR, 2013)

Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications. - Masaki Nakamura 001; Kazuhiro Ogata 001; Kokichi Futatsugi (Specification, Algebra, and Software, 2014)

Proving Sufficient Completeness of Constructor-Based Algebraic Specifications. - Masaki Nakamura 001; Daniel Gâinâ; Kazuhiro Ogata 001; Kokichi Futatsugi (CSA/CUTE, 2015)

The visualization system of center of pressure and base of support in sit-to-stand movement. - Masaki Nakamura 001; Akira Urashima; Tomoji Toriyama; Toshihiro Ninomiya; Noriyuki Fukumoto; Yuuki Aiboshi (GCCE, 2015)

A preliminary study of test case generation by CafeOBJ rewrite specifications. - Masaki Nakamura 001 (GCCE, 2016)

Automated Test Case Generation from OTS/CafeOBJ Specifications by Specification Translation. - Ryusei Mori; Masaki Nakamura 001 (ICST Workshops, 2017)

Foreword. - Masaki Nakamura 001 (IEICE Trans. Inf. Syst., 2017)

Formal Verification and Mathematical Optimization for Autonomous Vehicle Group Controllers. - Masaki Nakamura 001; Kazutoshi Sakakibara (MoDELS (Companion), 2019)

Formal verification of Fischer's real-time mutual exclusion protocol by the OTS/CafeOBJ method. - Masaki Nakamura 001; Shuki Higashi; Kazutoshi Sakakibara; Kazuhiro Ogata 001 (SICE, 2020)

Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method. - Masaki Nakamura 001; Kazutoshi Sakakibara; Kazuhiro Ogata 001 (CoRR, 2020)

Stability of termination and sufficient-completeness under pushouts via amalgamation. - Daniel Gaina; Masaki Nakamura 001; Kazuhiro Ogata 001; Kokichi Futatsugi (Theor. Comput. Sci., 2020)

Formal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method. - Masaki Nakamura 001; Kazutoshi Sakakibara; Yuki Okura; Kazuhiro Ogata 001 (Int. J. Softw. Eng. Knowl. Eng., 2021)

An Investigation of Formal Verification of Control Policy of Multi-Car Elevator Systems Using Statistical Model Checking. - Yuki Kitahara; Masaki Nakamura 001; Kazutoshi Sakakibara (ICMLC, 2022)

Toward Prediction of Traffic Accidents Using Formal Concept Analysis of Actual Accidents and Related Data. - Shogo Kotani; Masaki Nakamura 001; Kazutoshi Sakakibara; Tatsuo Motoyoshi; Keisuke Hoshikawa (ICMLC, 2022)

The MIP-Based Large Neighborhood Local Search Method for Large-Scale Optimization Problems with Many Constraints: Application to the Machining Scheduling. - Jin Matsuzaki; Kazutoshi Sakakibara; Masaki Nakamura 001 (ICMLC, 2022)

Machine Learning for Protein Solubility Prediction. - Kodai Suzuki; Kazutoshi Sakakibara; Masaki Nakamura 001; Suguru Shinoda; Yasuhisa Asano (ICMLC, 2022)

Formal Verification of the Lim-Jeong-Park-Lee Autonomous Vehicle Control Protocol using the OTS/CafeOBJ Method. - Tatsuya Igarashi; Masaki Nakamura 001; Kazutoshi Sakakibara (SEKE, 2022)

Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method. - Masaki Nakamura 001; Shuki Higashi; Kazutoshi Sakakibara; Kazuhiro Ogata 001 (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2022)

Formal Specification and Verification of an Autonomous Vehicle Control System by the OTS/CafeOBJ method (S). - Yifan Wang; Masaki Nakamura 001; Kazutoshi Sakakibara; Yuki Okura (SEKE, 2023)

Modeling and Verification of Variable Multi-Lane Intersection Controls for Autonomous Vehicles Using Uppaal SMC. - Akihito Hachiro; Masaki Nakamura 001; Kazutoshi Sakakibara; Takuya Matsumoto; Ryo Takano (ICMLC, 2024)

Formal Concept Analysis for Traffic Accident Summaries and Construction of Traffic Accident Prediction Model. - Haruto Murakami; Kazutoshi Sakakibara; Masaki Nakamura 001; Tatsuo Motoyoshi; Keisuke Hoshikawa; Takuya Matsumoto; Ryo Takano (ICMLC, 2024)

Investigation of Formal Verification of Autonomous Vehicle Control Systems Through Specification Translation from Cafeobj to Real-Time Maude. - Yifan Wang; Masaki Nakamura 001; Ryo Takano; Takuya Matsumoto; Kazutoshi Sakakibara (ICMLC, 2024)

Large neighborhood local search method with MIP techniques for large-scale machining scheduling with many constraints. - Jin Matsuzaki; Kazutoshi Sakakibara; Masaki Nakamura 001; Shinya Watanabe (J. Supercomput., 2024)

Proof Scores: A Survey (full version). - Adrián Riesco 001; Kazuhiro Ogata 001; Masaki Nakamura 001; Daniel Gaina; Duong Dinh Tran; Kokichi Futatsugi (CoRR, 2025)

Proof Scores: A Survey. - Adrián Riesco 001; Kazuhiro Ogata 001; Masaki Nakamura 001; Daniel Gaina; Duong Dinh Tran; Kokichi Futatsugi (ACM Comput. Surv., 2025)