| 2025 | KES | Annotated Evidential Linear-time Temporal Logic. | Yotaro Nakayama, Yoshitaka Aoki, Seiki Akama |
| 2020 | SAC | A model transformation approach to constructing agent-oriented design models for CPS/IoT systems. | Hiroyuki Nakagawa, Shinpei Ogata, Yoshitaka Aoki, Kazuki Kobayashi |
| 2018 | APSEC | Verification of CPS Based on Control Loop Using Model Checking. | Yoshitaka Aoki, Shinpei Ogata, Kazuki Kobayashi, Hiroyuki Nakagawa |
| 2018 | ENASE | Goal-Satisfaction Verification to Combination of Use Case Components. | Saeko Matsuura, Shinpei Ogata, Yoshitaka Aoki |
| 2018 | PRIMA | A Template System for Modeling and Verifying Agent Behaviors. | Shinpei Ogata, Yoshitaka Aoki, Hiroyuki Nakagawa, Kazuki Kobayashi |
| 2017 | MODELS | A Tool to Edit and Verify IoT System Architecture Model. | Shinpei Ogata, Hiroyuki Nakagawa, Yoshitaka Aoki, Kazuki Kobayashi, Yuko Fukushima |
| 2017 | MODELSWARD | Security Requirements Verification for Existing Systems with Model Checking Technique and UML. | Saeko Matsuura, Shinpei Ogata, Yoshitaka Aoki |
| 2014 | ISSRE | Practical Behavioral Inconsistency Detection between Source Code and Specification Using Model Checking. | Saeko Matsuura, Yoshitaka Aoki, Shinpei Ogata |
| 2014 | RE | Verifying security requirements using model checking technique for UML-based requirements specification. | Yoshitaka Aoki, Saeko Matsuura |
| 2010 | COMPSAC | A Method for Detecting Defects in Source Codes Using Model Checking Techniques. | Yoshitaka Aoki, Saeko Matsuura |