Akihisa Yamada

74 papers A* 1A 6B 14C 3Misc 2Journal 38Unranked 10

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Sorted Rewriting, Conditional Rewriting, and Logically Constrained Rewriting. Arch. Formal Proofs Akihisa Yamada
2025	B	`conf`	An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. CPP Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada
2025	J	`jnl`	Context-Free Grammars and Languages. Arch. Formal Proofs Tobias Nipkow, Markus Gschoßmann, Felix Krayer, Fabian Lehr, Bruno Philipp, August Martin Stimpfle, Kaan Taskin, Akihisa Yamada
2025	J	`jnl`	First-Order Rewriting. Arch. Formal Proofs René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler, Akihisa Yamada
2025	J	`jnl`	Greibach Normal Form. Arch. Formal Proofs Alexander Haberl, Tobias Nipkow, Akihisa Yamada
2025	—	`conf`	Weighted Rewriting. FroCoS Martin Avanzini, Akihisa Yamada
2024	B	`conf`	A Verified Algorithm for Deciding Pattern Completeness. FSCD René Thiemann, Akihisa Yamada
2024	C	`conf`	Goal-Aware RSS for Complex Scenarios via Program Logic. IV Ichiro Hasuo, Clovis Eberhart, James Haydon, Jérémy Dubut, Rose Bohrer, Tsutomu Kobayashi, Sasinee Pruekprasert, Xiao-Yi Zhang, Erik André Pallas, Akihisa Yamada, Kohei Suenaga, Fuyuki Ishikawa, Kenji Kamijo, Yoshiyuki Shinya, Takamasa Suetomi
2024	—	`conf`	Hedge Automata Revisited: Transforming Texts to and from XML. ATVA (2) Akihisa Yamada, Jérémy Dubut, Takeshi Tsukada
2024	J	`jnl`	Sorted Terms. Arch. Formal Proofs Akihisa Yamada, René Thiemann
2024	J	`jnl`	Verifying a Decision Procedure for Pattern Completeness. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2023	B	`conf`	Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). ITP Akihisa Yamada, Jérémy Dubut
2023	J	`jnl`	Formalizing Results on Directed Sets. Arch. Formal Proofs Akihisa Yamada, Jérémy Dubut
2023	J	`jnl`	Goal-Aware RSS for Complex Scenarios via Program Logic. IEEE Trans. Intell. Veh. Ichiro Hasuo, Clovis Eberhart, James Haydon, Jérémy Dubut, Rose Bohrer, Tsutomu Kobayashi, Sasinee Pruekprasert, Xiao-Yi Zhang, Erik André Pallas, Akihisa Yamada, Kohei Suenaga, Fuyuki Ishikawa, Kenji Kamijo, Yoshiyuki Shinya, Takamasa Suetomi
2023	B	`conf`	Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). FSCD Akihisa Yamada
2023	J	`jnl`	The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions. CoRR Akihisa Yamada, Benjamin Lucien Kaminski, Dieter Hofbauer, Fred Mesnard, Étienne Payet
2022	J	`jnl`	Fixed Points Theorems for Non-Transitive Relations. Log. Methods Comput. Sci. Jérémy Dubut, Akihisa Yamada
2022	J	`jnl`	Goal-Aware RSS for Complex Scenarios via Program Logic. CoRR Ichiro Hasuo, Clovis Eberhart, James Haydon, Jérémy Dubut, Rose Bohrer, Tsutomu Kobayashi, Sasinee Pruekprasert, Xiao-Yi Zhang, Erik André Pallas, Akihisa Yamada, Kohei Suenaga, Fuyuki Ishikawa, Kenji Kamijo, Yoshiyuki Shinya, Takamasa Suetomi
2022	A	`conf`	Term Orderings for Non-reachability of (Conditional) Rewriting. IJCAR Akihisa Yamada
2022	J	`jnl`	Tuple Interpretations for Termination of Term Rewriting. J. Autom. Reason. Akihisa Yamada
2021	J	`jnl`	A Formalization of Weighted Path Orders and Recursive Path Orders. Arch. Formal Proofs Christian Sternagel, René Thiemann, Akihisa Yamada
2021	J	`jnl`	Architecture-Guided Test Resource Allocation Via Logic. CoRR Clovis Eberhart, Akihisa Yamada, Stefan Klikovits, Shin-ya Katsumata, Tsutomu Kobayashi, Ichiro Hasuo, Fuyuki Ishikawa
2021	—	`conf`	Architecture-Guided Test Resource Allocation via Logic. TAP@STAF Clovis Eberhart, Akihisa Yamada, Stefan Klikovits, Shin-ya Katsumata, Tsutomu Kobayashi, Ichiro Hasuo, Fuyuki Ishikawa
2021	A	`conf`	Multi-Dimensional Interpretations for Termination of Term Rewriting. CADE Akihisa Yamada
2020	J	`jnl`	A Verified Implementation of Algebraic Numbers in Isabelle/HOL. J. Autom. Reason. Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2020	J	`jnl`	A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. J. Autom. Reason. Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2020	B	`conf`	Certifying the Weighted Path Order (Invited Talk). FSCD René Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
2020	J	`jnl`	Fixed Points Theorems for Non-Transitive Relations. CoRR Jérémy Dubut, Akihisa Yamada
2020	J	`jnl`	Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. J. Autom. Reason. René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada
2020	J	`jnl`	On probabilistic term rewriting. Sci. Comput. Program. Martin Avanzini, Ugo Dal Lago, Akihisa Yamada
2020	—	`conf`	Relational Differential Dynamic Logic. TACAS (1) Juraj Kolcák, Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata, David Sprunger, Akihisa Yamada
2019	B	`conf`	Complete Non-Orders and Fixed Points. ITP Akihisa Yamada, Jérémy Dubut
2019	J	`jnl`	Complete Non-Orders and Fixed Points. Arch. Formal Proofs Akihisa Yamada, Jérémy Dubut
2019	—	`conf`	Reachability Analysis for Termination and Confluence of Rewriting. TACAS (1) Christian Sternagel, Akihisa Yamada
2019	J	`jnl`	Relational Differential Dynamic Logic. CoRR Juraj Kolcák, Ichiro Hasuo, Jérémy Dubut, Shin-ya Katsumata, David Sprunger, Akihisa Yamada
2019	—	`conf`	Relational differential dynamic logic: poster abstract. HSCC Juraj Kolcák, Ichiro Hasuo, Jérémy Dubut, Shin-ya Katsumata, David Sprunger, Akihisa Yamada
2019	—	`conf`	Scenario Sampling for Cyber Physical Systems using Combinatorial Testing. ICST Workshops Akihisa Yamada, Clovis Eberhart, Fuyuki Ishikawa, Nian-Ze Lee
2019	—	`conf`	TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, Akihisa Yamada
2019	—	`conf`	The Termination and Complexity Competition. TACAS (3) Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
2018	B	`conf`	A Formalization of the LLL Basis Reduction Algorithm. ITP Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2018	J	`jnl`	A verified LLL algorithm. Arch. Formal Proofs Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2018	J	`jnl`	A verified factorization algorithm for integer polynomials with polynomial complexity. Arch. Formal Proofs Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2018	B	`conf`	Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). CPP Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada
2018	Misc	`conf`	On Probabilistic Term Rewriting. FLOPS Martin Avanzini, Ugo Dal Lago, Akihisa Yamada
2018	J	`jnl`	On Probabilistic Term Rewriting. CoRR Martin Avanzini, Ugo Dal Lago, Akihisa Yamada
2017	B	`conf`	A formalization of the Berlekamp-Zassenhaus factorization algorithm. CPP Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2017	A	`conf`	Certifying Safety and Termination Proofs for Integer Transition Systems. CADE Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2017	B	`conf`	Classification Tree Method with Parameter Shielding. SAFECOMP Takashi Kitamura, Akihisa Yamada, Goro Hatayama, Shinya Sakuragi, Eun-Hye Choi, Cyrille Artho
2017	J	`jnl`	Relative Termination via Dependency Pairs. J. Autom. Reason. José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
2017	J	`jnl`	Subresultants. Arch. Formal Proofs Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2016	B	`conf`	AC Dependency Pairs Revisited. CSL Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari
2016	J	`jnl`	AC-KBO revisited. Theory Pract. Log. Program. Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp
2016	B	`conf`	Algebraic Numbers in Isabelle/HOL. ITP René Thiemann, Akihisa Yamada
2016	A	`conf`	Distance-Integrated Combinatorial Testing. ISSRE Eun-Hye Choi, Cyrille Artho, Takashi Kitamura, Osamu Mizuno, Akihisa Yamada
2016	B	`conf`	Formalizing jordan normal forms in Isabelle/HOL. CPP René Thiemann, Akihisa Yamada
2016	A*	`conf`	Greedy combinatorial test case generation using unsatisfiable cores. ASE Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, Eun-Hye Choi
2016	J	`jnl`	Perron-Frobenius Theorem for Spectral Radius Analysis. Arch. Formal Proofs Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada
2016	J	`jnl`	Polynomial Factorization. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2016	J	`jnl`	Polynomial Interpolation. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2016	J	`jnl`	The Factorization Algorithm of Berlekamp and Zassenhaus. Arch. Formal Proofs Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2015	J	`jnl`	A unified ordering for termination proving. Sci. Comput. Program. Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
2015	J	`jnl`	Algebraic Numbers in Isabelle/HOL. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2015	C	`conf`	Combinatorial Testing for Tree-Structured Test Models with Constraints. QRS Takashi Kitamura, Akihisa Yamada, Goro Hatayama, Cyrille Artho, Eun-Hye Choi, Thi Bich Ngoc Do, Yutaka Oiwa, Shinya Sakuragi
2015	J	`jnl`	Matrices, Jordan Normal Forms, and Spectral Radius Theory. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2015	A	`conf`	Optimization of Combinatorial Testing by Incremental SAT Solving. ICST Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-Hye Choi, Yutaka Oiwa, Armin Biere
2015	B	`conf`	Priority Integration for Weighted Combinatorial Testing. COMPSAC Eun-Hye Choi, Takashi Kitamura, Cyrille Artho, Akihisa Yamada, Yutaka Oiwa
2015	A	`conf`	Reducing Relative Termination to Dependency Pair Problems. CADE José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
2014	J	`jnl`	A Unified Ordering for Termination Proving. CoRR Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
2014	Misc	`conf`	AC-KBO Revisited. FLOPS Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp
2014	J	`jnl`	AC-KBO Revisited. CoRR Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp
2014	—	`conf`	Nagoya Termination Tool. RTA-TLCA Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
2014	J	`jnl`	Nagoya Termination Tool. CoRR Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
2013	C	`conf`	Unifying the Knuth-Bendix, recursive path and polynomial orders. PPDP Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
2012	J	`jnl`	A Sound Type System for Typing Runtime Errors. Inf. Media Technol. Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, Naoki Nishida