A Sound Type System for Typing Runtime Errors. - Akihisa Yamada 002; Keiichirou Kusakari; Toshiki Sakabe; Masahiko Sakai; Naoki Nishida 001 (Inf. Media Technol., 2012)

Unifying the Knuth-Bendix, recursive path and polynomial orders. - Akihisa Yamada 002; Keiichirou Kusakari; Toshiki Sakabe (PPDP, 2013)

Nagoya Termination Tool. - Akihisa Yamada 002; Keiichirou Kusakari; Toshiki Sakabe (RTA-TLCA, 2014)

Reducing Relative Termination to Dependency Pair Problems. - José Iborra; Naoki Nishida 001; Germán Vidal; Akihisa Yamada 002 (CADE, 2015)

Priority Integration for Weighted Combinatorial Testing. - Eun-Hye Choi; Takashi Kitamura 001; Cyrille Artho; Akihisa Yamada 002; Yutaka Oiwa (COMPSAC, 2015)

Optimization of Combinatorial Testing by Incremental SAT Solving. - Akihisa Yamada 002; Takashi Kitamura 001; Cyrille Artho; Eun-Hye Choi; Yutaka Oiwa; Armin Biere (ICST, 2015)

Combinatorial Testing for Tree-Structured Test Models with Constraints. - Takashi Kitamura 001; Akihisa Yamada 002; Goro Hatayama; Cyrille Artho; Eun-Hye Choi; Thi Bich Ngoc Do; Yutaka Oiwa; Shinya Sakuragi (QRS, 2015)

Algebraic Numbers in Isabelle/HOL. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2015)

Matrices, Jordan Normal Forms, and Spectral Radius Theory. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2015)

A unified ordering for termination proving. - Akihisa Yamada 002; Keiichirou Kusakari; Toshiki Sakabe (Sci. Comput. Program., 2015)

Formalizing jordan normal forms in Isabelle/HOL. - René Thiemann; Akihisa Yamada 002 (CPP, 2016)

AC Dependency Pairs Revisited. - Akihisa Yamada 002; Christian Sternagel; René Thiemann; Keiichirou Kusakari (CSL, 2016)

Distance-Integrated Combinatorial Testing. - Eun-Hye Choi; Cyrille Artho; Takashi Kitamura 001; Osamu Mizuno; Akihisa Yamada 002 (ISSRE, 2016)

Greedy combinatorial test case generation using unsatisfiable cores. - Akihisa Yamada 002; Armin Biere; Cyrille Artho; Takashi Kitamura 001; Eun-Hye Choi (ASE, 2016)

The Factorization Algorithm of Berlekamp and Zassenhaus. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

Perron-Frobenius Theorem for Spectral Radius Analysis. - Jose Divasón; Ondrej Kuncar; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

Polynomial Factorization. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

Polynomial Interpolation. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

AC-KBO revisited. - Akihisa Yamada 002; Sarah Winkler; Nao Hirokawa; Aart Middeldorp (Theory Pract. Log. Program., 2016)

Certifying Safety and Termination Proofs for Integer Transition Systems. - Marc Brockschmidt; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (CADE, 2017)

A formalization of the Berlekamp-Zassenhaus factorization algorithm. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (CPP, 2017)

Classification Tree Method with Parameter Shielding. - Takashi Kitamura 001; Akihisa Yamada 002; Goro Hatayama; Shinya Sakuragi; Eun-Hye Choi; Cyrille Artho (SAFECOMP, 2017)

Subresultants. - Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2017)

Relative Termination via Dependency Pairs. - José Iborra; Naoki Nishida 001; Germán Vidal; Akihisa Yamada 002 (J. Autom. Reason., 2017)

Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). - Jose Divasón; Sebastiaan J. C. Joosten; Ondrej Kuncar; René Thiemann; Akihisa Yamada 002 (CPP, 2018)

A Formalization of the LLL Basis Reduction Algorithm. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (ITP, 2018)

A verified LLL algorithm. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2018)

A verified factorization algorithm for integer polynomials with polynomial complexity. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2018)

Relational differential dynamic logic: poster abstract. - Juraj Kolcák; Ichiro Hasuo; Jérémy Dubut; Shin-ya Katsumata; David Sprunger; Akihisa Yamada 002 (HSCC, 2019)

Scenario Sampling for Cyber Physical Systems using Combinatorial Testing. - Akihisa Yamada 002; Clovis Eberhart; Fuyuki Ishikawa; Nian-Ze Lee (ICST Workshops, 2019)

TOOLympics 2019: An Overview of Competitions in Formal Methods. - Ezio Bartocci; Dirk Beyer 001; Paul E. Black; Grigory Fedyukovich; Hubert Garavel; Arnd Hartmanns; Marieke Huisman; Fabrice Kordon; Julian Nagele; Mihaela Sighireanu; Bernhard Steffen; Martin Suda 001; et al. (TACAS (3), 2019)

The Termination and Complexity Competition. - Jürgen Giesl; Albert Rubio; Christian Sternagel; Johannes Waldmann; Akihisa Yamada 002 (TACAS (3), 2019)

Reachability Analysis for Termination and Confluence of Rewriting. - Christian Sternagel; Akihisa Yamada 002 (TACAS (1), 2019)

Complete Non-Orders and Fixed Points. - Akihisa Yamada 002; Jérémy Dubut (Arch. Formal Proofs, 2019)

Certifying the Weighted Path Order (Invited Talk). - René Thiemann; Jonas Schöpf; Christian Sternagel; Akihisa Yamada 002 (FSCD, 2020)

Relational Differential Dynamic Logic. - Juraj Kolcák; Jérémy Dubut; Ichiro Hasuo; Shin-ya Katsumata; David Sprunger; Akihisa Yamada 002 (TACAS (1), 2020)

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (J. Autom. Reason., 2020)

A Verified Implementation of Algebraic Numbers in Isabelle/HOL. - Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (J. Autom. Reason., 2020)

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. - René Thiemann; Ralph Bottesch; Jose Divasón; Max W. Haslbeck; Sebastiaan J. C. Joosten; Akihisa Yamada 002 (J. Autom. Reason., 2020)

On probabilistic term rewriting. - Martin Avanzini; Ugo Dal Lago; Akihisa Yamada 002 (Sci. Comput. Program., 2020)

Multi-Dimensional Interpretations for Termination of Term Rewriting. - Akihisa Yamada 002 (CADE, 2021)

Architecture-Guided Test Resource Allocation via Logic. - Clovis Eberhart; Akihisa Yamada 002; Stefan Klikovits; Shin-ya Katsumata; Tsutomu Kobayashi; Ichiro Hasuo; Fuyuki Ishikawa (TAP@STAF, 2021)

A Formalization of Weighted Path Orders and Recursive Path Orders. - Christian Sternagel; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2021)

Term Orderings for Non-reachability of (Conditional) Rewriting. - Akihisa Yamada 002 (IJCAR, 2022)

Tuple Interpretations for Termination of Term Rewriting. - Akihisa Yamada 002 (J. Autom. Reason., 2022)

Fixed Points Theorems for Non-Transitive Relations. - Jérémy Dubut; Akihisa Yamada 002 (Log. Methods Comput. Sci., 2022)

Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). - Akihisa Yamada 002 (FSCD, 2023)

Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). - Akihisa Yamada 002; Jérémy Dubut (ITP, 2023)

Formalizing Results on Directed Sets. - Akihisa Yamada 002; Jérémy Dubut (Arch. Formal Proofs, 2023)

The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions. - Akihisa Yamada 002; Benjamin Lucien Kaminski; Dieter Hofbauer; Fred Mesnard; Étienne Payet (CoRR, 2023)

Goal-Aware RSS for Complex Scenarios via Program Logic. - Ichiro Hasuo; Clovis Eberhart; James Haydon; Jérémy Dubut; Rose Bohrer; Tsutomu Kobayashi; Sasinee Pruekprasert; Xiao-Yi Zhang 005; Erik André Pallas; Akihisa Yamada 002; Kohei Suenaga; Fuyuki Ishikawa; et al. (IEEE Trans. Intell. Veh., 2023)

Hedge Automata Revisited: Transforming Texts to and from XML. - Akihisa Yamada 002; Jérémy Dubut; Takeshi Tsukada (ATVA (2), 2024)

A Verified Algorithm for Deciding Pattern Completeness. - René Thiemann; Akihisa Yamada 002 (FSCD, 2024)

Verifying a Decision Procedure for Pattern Completeness. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2024)

Sorted Terms. - Akihisa Yamada 002; René Thiemann (Arch. Formal Proofs, 2024)

An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. - Dohan Kim 001; Teppei Saito; René Thiemann; Akihisa Yamada 002 (CPP, 2025)

Context-Free Grammars and Languages. - Tobias Nipkow; Markus Gschoßmann; Felix Krayer; Fabian Lehr; Bruno Philipp; August Martin Stimpfle; Kaan Taskin; Akihisa Yamada 002 (Arch. Formal Proofs, 2025)

First-Order Rewriting. - René Thiemann; Christian Sternagel; Christina Kirk; Martin Avanzini; Bertram Felgenhauer; Julian Nagele; Thomas Sternagel; Sarah Winkler; Akihisa Yamada 002 (Arch. Formal Proofs, 2025)