default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAkihisa Yamada 0002
Person information
- affiliation: National Institute of Advanced Industrial Science and Technology (AIST), Japan
- affiliation: National Institute of Informatics, NII, Japan
- affiliation (former): University of Innsbruck, Austria
- affiliation (former): Nagoya University, Sakabe Lab.
Other persons with the same name
- Akihisa Yamada 0001 — Sharp Corporation, Japan
- Akihisa Yamada 0003 — Kyoto Institute of Technology, Japan
SPARQL queries 
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2026
[j29]Akihisa Yamada:
Sorted Rewriting, Conditional Rewriting, and Logically Constrained Rewriting. Arch. Formal Proofs 2026 (2026)- 2025
- [j28]Alexander Haberl, Tobias Nipkow, Akihisa Yamada:
Greibach Normal Form. Arch. Formal Proofs 2025 (2025) - [j27]Tobias Nipkow, Markus Gschoßmann, Felix Krayer, Fabian Lehr, Bruno Philipp, August Martin Stimpfle, Kaan Taskin, Akihisa Yamada:
Context-Free Grammars and Languages. Arch. Formal Proofs 2025 (2025) - [j26]René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler, Akihisa Yamada:
First-Order Rewriting. Arch. Formal Proofs 2025 (2025) - [c36]Dohan Kim
, Teppei Saito, René Thiemann, Akihisa Yamada:
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. CPP 2025: 272-282 - [c35]Martin Avanzini, Akihisa Yamada:
Weighted Rewriting. FroCoS 2025: 191-208 - 2024
- [j25]René Thiemann, Akihisa Yamada:
Verifying a Decision Procedure for Pattern Completeness. Arch. Formal Proofs 2024 (2024) - [j24]Akihisa Yamada, René Thiemann:
Sorted Terms. Arch. Formal Proofs 2024 (2024) - [c34]Akihisa Yamada, Jérémy Dubut, Takeshi Tsukada:
Hedge Automata Revisited: Transforming Texts to and from XML. ATVA (2) 2024: 117-136 - [c33]René Thiemann, Akihisa Yamada:
A Verified Algorithm for Deciding Pattern Completeness. FSCD 2024: 27:1-27:17 - [c32]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:
Goal-Aware RSS for Complex Scenarios via Program Logic. IV 2024: 3154 - 2023
- [j23]Akihisa Yamada, Jérémy Dubut:
Formalizing Results on Directed Sets. Arch. Formal Proofs 2023 (2023) - [j22]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:
Goal-Aware RSS for Complex Scenarios via Program Logic. IEEE Trans. Intell. Veh. 8(4): 3040-3072 (2023) - [c31]Akihisa Yamada:
Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). FSCD 2023: 4:1-4:5 - [c30]Akihisa Yamada, Jérémy Dubut:
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). ITP 2023: 34:1-34:13 - [i9]Akihisa Yamada, Benjamin Lucien Kaminski, Dieter Hofbauer, Fred Mesnard, Étienne Payet:
The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions. CoRR abs/2308.09536 (2023) - 2022
- [j21]Akihisa Yamada:
Tuple Interpretations for Termination of Term Rewriting. J. Autom. Reason. 66(4): 667-688 (2022) - [j20]Jérémy Dubut, Akihisa Yamada:
Fixed Points Theorems for Non-Transitive Relations. Log. Methods Comput. Sci. 18(1) (2022) - [c29]Akihisa Yamada:
Term Orderings for Non-reachability of (Conditional) Rewriting. IJCAR 2022: 248-267 - [i8]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:
Goal-Aware RSS for Complex Scenarios via Program Logic. CoRR abs/2207.02387 (2022) - 2021
- [j19]Christian Sternagel, René Thiemann, Akihisa Yamada:
A Formalization of Weighted Path Orders and Recursive Path Orders. Arch. Formal Proofs 2021 (2021) - [c28]Akihisa Yamada:
Multi-Dimensional Interpretations for Termination of Term Rewriting. CADE 2021: 273-290 - [c27]Clovis Eberhart, Akihisa Yamada, Stefan Klikovits, Shin-ya Katsumata, Tsutomu Kobayashi, Ichiro Hasuo, Fuyuki Ishikawa:
Architecture-Guided Test Resource Allocation via Logic. TAP@STAF 2021: 22-38 - [i7]Clovis Eberhart, Akihisa Yamada, Stefan Klikovits, Shin-ya Katsumata, Tsutomu Kobayashi, Ichiro Hasuo, Fuyuki Ishikawa:
Architecture-Guided Test Resource Allocation Via Logic. CoRR abs/2107.10948 (2021) - 2020
- [j18]Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Verified Implementation of Algebraic Numbers in Isabelle/HOL. J. Autom. Reason. 64(3): 363-389 (2020) - [j17]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. J. Autom. Reason. 64(4): 699-735 (2020) - [j16]René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada:
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. J. Autom. Reason. 64(5): 827-856 (2020) - [j15]Martin Avanzini, Ugo Dal Lago, Akihisa Yamada:
On probabilistic term rewriting. Sci. Comput. Program. 185 (2020) - [c26]René Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada:
Certifying the Weighted Path Order (Invited Talk). FSCD 2020: 4:1-4:20 - [c25]Juraj Kolcák, Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata, David Sprunger, Akihisa Yamada:
Relational Differential Dynamic Logic. TACAS (1) 2020: 191-208 - [i6]Jérémy Dubut, Akihisa Yamada:
Fixed Points Theorems for Non-Transitive Relations. CoRR abs/2009.13065 (2020)
2010 – 2019
- 2019
- [j14]Akihisa Yamada, Jérémy Dubut:
Complete Non-Orders and Fixed Points. Arch. Formal Proofs 2019 (2019) - [c24]Juraj Kolcák, Ichiro Hasuo, Jérémy Dubut, Shin-ya Katsumata, David Sprunger, Akihisa Yamada:
Relational differential dynamic logic: poster abstract. HSCC 2019: 284-285 - [c23]Akihisa Yamada, Clovis Eberhart, Fuyuki Ishikawa, Nian-Ze Lee:
Scenario Sampling for Cyber Physical Systems using Combinatorial Testing. ICST Workshops 2019: 198-199 - [c22]Akihisa Yamada, Jérémy Dubut:
Complete Non-Orders and Fixed Points. ITP 2019: 30:1-30:16 - [c21]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:
TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) 2019: 3-24 - [c20]Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada:
The Termination and Complexity Competition. TACAS (3) 2019: 156-166 - [c19]Christian Sternagel, Akihisa Yamada:
Reachability Analysis for Termination and Confluence of Rewriting. TACAS (1) 2019: 262-278 - [i5]Juraj Kolcák, Ichiro Hasuo, Jérémy Dubut, Shin-ya Katsumata, David Sprunger, Akihisa Yamada:
Relational Differential Dynamic Logic. CoRR abs/1903.00153 (2019) - 2018
- [j13]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A verified LLL algorithm. Arch. Formal Proofs 2018 (2018) - [j12]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A verified factorization algorithm for integer polynomials with polynomial complexity. Arch. Formal Proofs 2018 (2018) - [c18]Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). CPP 2018: 2-13 - [c17]Martin Avanzini, Ugo Dal Lago, Akihisa Yamada:
On Probabilistic Term Rewriting. FLOPS 2018: 132-148 - [c16]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Formalization of the LLL Basis Reduction Algorithm. ITP 2018: 160-177 - [i4]Martin Avanzini, Ugo Dal Lago, Akihisa Yamada:
On Probabilistic Term Rewriting. CoRR abs/1802.09774 (2018) - 2017
- [j11]Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
Subresultants. Arch. Formal Proofs 2017 (2017) - [j10]José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada:
Relative Termination via Dependency Pairs. J. Autom. Reason. 58(3): 391-411 (2017) - [c15]Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
Certifying Safety and Termination Proofs for Integer Transition Systems. CADE 2017: 454-471 - [c14]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A formalization of the Berlekamp-Zassenhaus factorization algorithm. CPP 2017: 17-29 - [c13]Takashi Kitamura, Akihisa Yamada, Goro Hatayama, Shinya Sakuragi, Eun-Hye Choi, Cyrille Artho:
Classification Tree Method with Parameter Shielding. SAFECOMP 2017: 230-241 - 2016
- [j9]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
The Factorization Algorithm of Berlekamp and Zassenhaus. Arch. Formal Proofs 2016 (2016) - [j8]Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
Perron-Frobenius Theorem for Spectral Radius Analysis. Arch. Formal Proofs 2016 (2016) - [j7]René Thiemann, Akihisa Yamada:
Polynomial Factorization. Arch. Formal Proofs 2016 (2016) - [j6]René Thiemann, Akihisa Yamada:
Polynomial Interpolation. Arch. Formal Proofs 2016 (2016) - [j5]Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
AC-KBO revisited. Theory Pract. Log. Program. 16(2): 163-188 (2016) - [c12]René Thiemann, Akihisa Yamada:
Formalizing jordan normal forms in Isabelle/HOL. CPP 2016: 88-99 - [c11]Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari:
AC Dependency Pairs Revisited. CSL 2016: 8:1-8:16 - [c10]Eun-Hye Choi, Cyrille Artho, Takashi Kitamura, Osamu Mizuno, Akihisa Yamada:
Distance-Integrated Combinatorial Testing. ISSRE 2016: 93-104 - [c9]René Thiemann, Akihisa Yamada:
Algebraic Numbers in Isabelle/HOL. ITP 2016: 391-408 - [c8]Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, Eun-Hye Choi:
Greedy combinatorial test case generation using unsatisfiable cores. ASE 2016: 614-624 - 2015
- [j4]René Thiemann, Akihisa Yamada:
Algebraic Numbers in Isabelle/HOL. Arch. Formal Proofs 2015 (2015) - [j3]René Thiemann, Akihisa Yamada:
Matrices, Jordan Normal Forms, and Spectral Radius Theory. Arch. Formal Proofs 2015 (2015) - [j2]Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
A unified ordering for termination proving. Sci. Comput. Program. 111: 110-134 (2015) - [c7]José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada:
Reducing Relative Termination to Dependency Pair Problems. CADE 2015: 163-178 - [c6]Eun-Hye Choi, Takashi Kitamura, Cyrille Artho, Akihisa Yamada, Yutaka Oiwa:
Priority Integration for Weighted Combinatorial Testing. COMPSAC 2015: 242-247 - [c5]Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-Hye Choi, Yutaka Oiwa, Armin Biere:
Optimization of Combinatorial Testing by Incremental SAT Solving. ICST 2015: 1-10 - [c4]Takashi Kitamura, Akihisa Yamada, Goro Hatayama, Cyrille Artho, Eun-Hye Choi, Thi Bich Ngoc Do, Yutaka Oiwa, Shinya Sakuragi:
Combinatorial Testing for Tree-Structured Test Models with Constraints. QRS 2015: 141-150 - 2014
- [c3]Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
AC-KBO Revisited. FLOPS 2014: 319-335 - [c2]Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
Nagoya Termination Tool. RTA-TLCA 2014: 466-475 - [i3]Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
AC-KBO Revisited. CoRR abs/1403.0406 (2014) - [i2]Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
A Unified Ordering for Termination Proving. CoRR abs/1404.6245 (2014) - [i1]Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
Nagoya Termination Tool. CoRR abs/1404.6626 (2014) - 2013
- [c1]Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
Unifying the Knuth-Bendix, recursive path and polynomial orders. PPDP 2013: 181-192 - 2012
- [j1]Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, Naoki Nishida:
A Sound Type System for Typing Runtime Errors. Inf. Media Technol. 7(2): 667-675 (2012)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2026-04-24 00:19 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
