A Decision Procedure for the Alternation-Free Two-Way Modal µ-Calculus. - Yoshinori Tanabe; Koichi Takahashi; Mitsuharu Yamamoto; Akihiko Tozawa; Masami Hagiya (TABLEAUX, 2005)

Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification. - Mitsuharu Yamamoto; Yoshinori Tanabe; Koichi Takahashi; Masami Hagiya (VSTTE, 2005)

A decision procedure for alternation-free modal µ-calculi. - Yoshinori Tanabe; Koichi Takahashi; Masami Hagiya (Advances in Modal Logic, 2008)

Architecture-aware Partial Order Reduction to Accelerate Model Checking of Networked Programs. - Cyrille Artho; Watcharin Leungwattanakit; Masami Hagiya; Yoshinori Tanabe (SNPD, 2008)

Tools and Techniques for Model Checking Networked Programs. - Cyrille Artho; Watcharin Leungwattanakit; Masami Hagiya; Yoshinori Tanabe (SNPD, 2008)

Efficient Model Checking of Networked Applications. - Cyrille Artho; Watcharin Leungwattanakit; Masami Hagiya; Yoshinori Tanabe (TOOLS (46), 2008)

Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic. - Yoshifumi Yuasa; Yoshinori Tanabe; Toshifusa Sekizawa; Koichi Takahashi (VSTTE, 2008)

Fixed-Point Computations over Functions on Integers with Operations min, max and plus. - Yoshinori Tanabe; Masami Hagiya (FICS, 2009)

Verifying networked programs using a model checker extension. - Watcharin Leungwattanakit; Cyrille Artho; Masami Hagiya; Yoshinori Tanabe; Mitsuharu Yamamoto (ICSE Companion, 2009)

Cache-Based Model Checking of Networked Applications: From Linear to Branching Time. - Cyrille Artho; Watcharin Leungwattanakit; Masami Hagiya; Yoshinori Tanabe; Mitsuharu Yamamoto (ASE, 2009)

Introduction of Virtualization Technology to Multi-Process Model Checking. - Watcharin Leungwattanakit; Cyrille Valentin Artho; Masami Hagiya; Yoshinori Tanabe; Mitsuharu Yamamoto (NASA Formal Methods, 2009)

Pre- and Post-Conditions Expressed in Variants of the Modal µ-Calculus. - Yoshinori Tanabe; Toshifusa Sekizawa; Yoshifumi Yuasa; Koichi Takahashi (IEICE Trans. Inf. Syst., 2009)

Model Checking of Concurrent Algorithms: From Java to C. - Cyrille Artho; Masami Hagiya; Watcharin Leungwattanakit; Yoshinori Tanabe; Mitsuharu Yamamoto (DIPES/BICC, 2010)

Decidability and Undecidability Results on the Modal µ-Calculus with a Natural Number-Valued Semantics. - Alexis Goyet; Masami Hagiya; Yoshinori Tanabe (WoLLIC, 2010)

Modal μ-calculus on Min-plus Algebra N∞. - Dai Ikarashi; Yoshinori Tanabe; Koki Nishizawa; Masami Hagiya (Inf. Media Technol., 2010)

Model checking distributed systems by combining caching and process checkpointing. - Watcharin Leungwattanakit; Cyrille Artho; Masami Hagiya; Yoshinori Tanabe; Mitsuharu Yamamoto (ASE, 2011)

Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications. - Kosuke Ono; Yoichi Hirai; Yoshinori Tanabe; Natsuko Noda; Masami Hagiya (SEFM, 2011)

Modbat: A Model-Based API Tester for Event-Driven Systems. - Cyrille Valentin Artho; Armin Biere; Masami Hagiya; Eric Platon; Martina Seidl; Yoshinori Tanabe; Mitsuharu Yamamoto (Haifa Verification Conference, 2013)

Software model checking for distributed systems with selector-based, non-blocking communication. - Cyrille Artho; Masami Hagiya; Richard Potter; Yoshinori Tanabe; Franz Weitl; Mitsuharu Yamamoto (ASE, 2013)

Automated verification of pattern-based interaction invariants in Ajax applications. - Yuta Maezawa; Hironori Washizaki; Yoshinori Tanabe; Shinichi Honiden (ASE, 2013)

Modular Software Model Checking for Distributed Systems. - Watcharin Leungwattanakit; Cyrille Artho; Masami Hagiya; Yoshinori Tanabe; Mitsuharu Yamamoto; Koichi Takahashi (IEEE Trans. Software Eng., 2014)

Pedagogical Lessons from an International Collaborative Big Data Undergraduate Research Project. - Graham Collins; Hugh Varilly; Yoshinori Tanabe (ECSA Workshops, 2015)

Keys and Roles of Formal Methods Education for Industry: 10 Year Experience with Top SE Program. - Fuyuki Ishikawa; Nobukazu Yoshioka; Yoshinori Tanabe (FMSEE&T@FM, 2015)

GRT at the SBST 2015 Tool Competition. - Lei Ma 003; Cyrille Artho; Cheng Zhang; Hiroyuki Sato; Masami Hagiya; Yoshinori Tanabe; Mitsuharu Yamamoto (SBST@ICSE, 2015)

Cardinality of UDP Transmission Outcomes. - Franz Weitl; Nazim Sebih; Cyrille Artho; Masami Hagiya; Yoshinori Tanabe; Yoriyuki Yamagata; Mitsuharu Yamamoto (SETTA, 2015)

Using Checkpointing and Virtualization for Fault Injection. - Cyrille Artho; Kuniyasu Suzaki; Masami Hagiya; Watcharin Leungwattanakit; Richard Potter; Eric Platon; Yoshinori Tanabe; Franz Weitl; Mitsuharu Yamamoto (Int. J. Netw. Comput., 2015)

Software Model Checking of UDP-based Distributed Applications. - Nazim Sebih; Masami Hagiya; Franz Weitl; Mitsuharu Yamamoto; Cyrille Artho; Yoshinori Tanabe (Int. J. Netw. Comput., 2015)

Runtime Monitoring for Concurrent Systems. - Yoriyuki Yamagata; Cyrille Artho; Masami Hagiya; Jun Inoue 001; Lei Ma 003; Yoshinori Tanabe; Mitsuharu Yamamoto (RV, 2016)

Java Pathfinder on Android Devices. - Alexander Kohan; Mitsuharu Yamamoto; Cyrille Artho; Yoriyuki Yamagata; Lei Ma 003; Masami Hagiya; Yoshinori Tanabe (ACM SIGSOFT Softw. Eng. Notes, 2016)

Model-Based API Testing of Apache ZooKeeper. - Cyrille Artho; Quentin Gros; Guillaume Rousset; Kazuaki Banzai; Lei Ma 003; Takashi Kitamura 001; Masami Hagiya; Yoshinori Tanabe; Mitsuharu Yamamoto (ICST, 2017)

Model-based Network Fault Injection for IoT Protocols. - Jun Yoneyama; Cyrille Artho; Yoshinori Tanabe; Masami Hagiya (ENASE, 2019)

Automatically Generating Programming Questions Corresponding to Rubrics Using Assertions and Invariants. - Masami Hagiya; Kosuke Fukuda; Yoshinori Tanabe; Toshinori Saito (SUZA, 2019)

Model-Based Testing for MQTT Applications. - Kotaro Tanabe; Yoshinori Tanabe; Masami Hagiya (JCKBSE, 2020)

Automated Detection of Respiratory Movements for Image Quality Assurance. - Yoshinori Tanabe; Takayuki Ishida (J. Medical Imaging Health Informatics, 2020)

Model-based testing of Apache ZooKeeper: Fundamental API usage and watchers. - Cyrille Artho; Kazuaki Banzai; Quentin Gros; Guillaume Rousset; Lei Ma 003; Takashi Kitamura 001; Masami Hagiya; Yoshinori Tanabe; Mitsuharu Yamamoto (Softw. Test. Verification Reliab., 2020)

Development of a Quantitative Method Based on the Hill-Shading Technique for Assessing Morphological Changes in the Bone During Image-Guided Radiotherapy for Bone Metastasis. - Yoshinori Tanabe; Takayuki Ishida (J. Medical Imaging Health Informatics, 2021)

Automatic Scoring in Programming Examinations for Beginners. - Yoshinori Tanabe; Masami Hagiya (JCKBSE, 2022)

A System for Programming Examinations with Block Components. - Yoshinori Tanabe (OCCE, 2024)