Collaboration-based verification of Object-Oriented models in HOL. - Kenro Yatake; Toshiaki Aoki; Takuya Katayama (VVEIS, 2004)

Implementing Application-Specific Object-Oriented Theories in HOL. - Kenro Yatake; Toshiaki Aoki; Takuya Katayama (ICTAC, 2005)

An Executable Semantics of Object-oriented Models for Simulation and Theorem Proving. - Kenro Yatake; Takuya Katayama (MSVVEIS, 2008)

Automatic Generation of Model Checking Scripts Based on Environment Modeling. - Kenro Yatake; Toshiaki Aoki (SPIN, 2010)

An executable object-oriented semantics and its application to firewall verification. - Kenro Yatake; Takuya Katayama (Softw. Syst. Model., 2011)

Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling. - Kenro Yatake; Toshiaki Aoki (ICTAC, 2012)

SMT-based enumeration of object graphs from UML class diagrams. - Kenro Yatake; Toshiaki Aoki (ACM SIGSOFT Softw. Eng. Notes, 2012)

SMT-Based Bounded Model Checking for OSEK/VDX Applications. - Haitao Zhang; Toshiaki Aoki; Hsin-Hung Lin; Min Zhang 002; Yuki Chiba; Kenro Yatake (APSEC (1), 2013)

An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol. - Xiaoyun Guo; Hsin-Hung Lin; Kenro Yatake; Toshiaki Aoki (FTSCS, 2013)

An Approach for Checking OSEK/VDX Applications. - Haitao Zhang; Toshiaki Aoki; Kenro Yatake; Min Zhang 002; Hsin-Hung Lin (QSIC, 2013)

Checking the Conformance of a Promela Design to its Formal Specification in Event-B. - Dieu-Huong Vu; Yuki Chiba; Kenro Yatake; Toshiaki Aoki (FTSCS, 2014)

A Framework for Verifying the Conformance of Design to Its Formal Specifications. - Dieu-Huong Vu; Yuki Chiba; Kenro Yatake; Toshiaki Aoki (IEICE Trans. Inf. Syst., 2015)

Verifying OSEK/VDX OS Design Using Its Formal Specification. - Dieu-Huong Vu; Yuki Chiba; Kenro Yatake; Toshiaki Aoki (TASE, 2016)