Kenro Yatake

Publication Activity (10 Years)

Years Active: 2004-2016
Publications (10 Years): 2

Top Topics

Linear Time Temporal Logic

Formal Specification

Top Venues

IEICE Trans. Inf. Syst.

Publications

Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
Verifying OSEK/VDX OS Design Using Its Formal Specification. TASE (2016)
Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
A Framework for Verifying the Conformance of Design to Its Formal Specifications. IEICE Trans. Inf. Syst. (6) (2015)
Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
Checking the Conformance of a Promela Design to its Formal Specification in Event-B. FTSCS (2014)
Xiaoyun Guo, Hsin-Hung Lin, Kenro Yatake, Toshiaki Aoki
An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol. FTSCS (2013)
Haitao Zhang, Toshiaki Aoki, Kenro Yatake, Min Zhang, Hsin-Hung Lin
An Approach for Checking OSEK/VDX Applications. QSIC (2013)
Haitao Zhang, Toshiaki Aoki, Hsin-Hung Lin, Min Zhang, Yuki Chiba, Kenro Yatake
SMT-Based Bounded Model Checking for OSEK/VDX Applications. APSEC (1) (2013)
Kenro Yatake, Toshiaki Aoki
Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling. ICTAC (2012)
Kenro Yatake, Toshiaki Aoki
SMT-based enumeration of object graphs from UML class diagrams. ACM SIGSOFT Softw. Eng. Notes 37 (4) (2012)
Kenro Yatake, Takuya Katayama
An executable object-oriented semantics and its application to firewall verification. Softw. Syst. Model. 10 (4) (2011)
Kenro Yatake, Toshiaki Aoki
Automatic Generation of Model Checking Scripts Based on Environment Modeling. SPIN (2010)
Kenro Yatake, Takuya Katayama
An Executable Semantics of Object-oriented Models for Simulation and Theorem Proving. MSVVEIS (2008)
Kenro Yatake, Toshiaki Aoki, Takuya Katayama
Implementing Application-Specific Object-Oriented Theories in HOL. ICTAC (2005)
Kenro Yatake, Toshiaki Aoki, Takuya Katayama
Collaboration-based verification of Object-Oriented models in HOL. VVEIS (2004)