YAMADA, Akihisa (山田晃久)

Research Interests

Affiliation

Apr. 2020current Senior researcher at Infrastructure Protection Security Research Team, Cyber Physical Security Research Center, AIST, Japan.
Nov. 2017Mar. 2020 Project assistant professor←postdoc at ERATO HASUO Metamathematics for Systems Design Project, National Institute of Informatics (NII), Japan.
Apr. 2015Oct. 2017 Postdoc at Computational Logic Group, University of Innsbruck, Austria.
May. 2014Mar. 2016 Visiting researcher←postdoc←technical staff at National Institute of Advanced Industiral Science (AIST), Japan.
Apr. 2011Sept. 2014 Ph.D. student at Sakabe-Sakai lab., Nagoya University, Japan.
Apr. 2008Mar. 2011 Engineer at Panasonic Advanced Technology Development Co, Ltd.
Apr. 2006Mar. 2008 Master student at Sakabe-Sakai lab.
Apr. 2002Mar. 2006 Bachelor student at Nagoya University.

Tools

I am the developer of and a contributor of

Publications

See also DBLP, Google Scholar, Research Gate, researchmap

Journal Articles

  1. Akihisa Yamada
    Tuple interpretations for termination of term rewriting JAR66667–6882022Invited, special issue for CADE-28. [Author's version]
  2. Ichiro HasuoClovis EberhartJames HaydonJérémy DubutRose BohrerTsutomu KobayshiSasinee PruekprasertXiao-Yi ZhangErik Andre PallasAkihisa YamadaKohei SuenagaFuyuki IshikawaKenji KamijoYoshiyuki ShinyaTakamasa Suetomi
    Goal-aware RSS for complex scenarios via program logic IEEE-IV843040–30722022
  3. Jérémy DubutAkihisa Yamada
    Fixed point theorems for non-transitive relations LMCS18(1:30)2022
  4. Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL JAR64: 827–856Springer2020 Invited, special issue for ITP 2018. [authors' version]
  5. On probabilistic term rewriting SCP185Elsevier. Invited, special issue for FLOPS 2018, online. [authors' version]
  6. A verified implementation of the Berlekamp–Zassenhaus factorization algorithm JAR64(4): 699–735Springer2020 [authors' version]
  7. A verified implementation of algebraic numbers in Isabelle/HOL JAR64:363–389Springer2020
  8. José IborraNaoki NishidaGermán VidalAkihisa Yamada
    Relative termination via dependency pairs JAR58(3):391–411Springer2017 Invited, special issue for CADE 2015.
  9. AC-KBO revisited TPLP16(2):163–188Cambridge University Press2016 Invited, special issue for FLOPS 2014. Also available as CoRR abs/1403.0406 errata
  10. A unified ordering for termination proving SCP111:110–134Elsevier2015 Invited, special issue for PPDP 2013. [arXiv version, expreiments].
  11. A sound type system for typing runtime errors IPSJ Transactions on Programming5(2):16–242012 Awarded IPSJ Tokai-branch student paper prize for encouragement.

Conference Papers

  1. Hedge automata revisited: Transforming texts to and from XML ATVA 20242024 to appear
  2. René ThiemannAkihisa Yamada
    A Verified Algorithm for Deciding Pattern Completeness FSCD 2024LIPIcs29927:1-27:172024
  3. Akihisa Yamada
    Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (invited talk) FSCD 2023LIPIcs2604:1–4:52023 [slides]
  4. Akihisa YamadaJérémy Dubut
    Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl) ITP 2023LIPIcs268pp. 34:1–34:132023
  5. Akihisa Yamada
    Term orderings for non-reachability of (conditional) rewriting IJCAR 2022LNAI13385pp. 248–2672022
  6. Akihisa Yamada
    Multi-dimensional interpretations for termination of term rewriting CADE-28LNAI12699pp. 273–2902021
  7. Architecture-guided test resource allocation via logic TAP 2021LNCS12740pp. 22–382021
  8. Certifying the weighted path order (invited talk) IJCAR-FSCD 2020LIPIcs1674:1–4:202020
  9. Relational differential dynamic logic TACAS 2020LNCS12078pp. 191–2082020
  10. Akihisa YamadaJérémy Dubut
    Complete non-orders and fixed points ITP 2019LIPIcs14130:1–30:162019
  11. Dirk BeyerEzio BartocciPaul E. BlackGrigory FedyukovichHubert GaravelArnd HartmannsMarieke HuismanFabrice KordonJulian NageleMihaela SighireanuBernhard SteffenMartin SudaGeoff SutcliffeTjark WeberAkihisa Yamada
    TOOLympics 2019: An overview of competitions in formal methods TACAS 2019 (3)LNCS11429pp. 3–242019
  12. The termination and complexity competition TACAS 2019 (3)LNCS11429pp. 156–1662019
  13. Christian SternagelAkihisa Yamada
    Reachability analysis for termination and confluence of rewriting TACAS 2019 (1), LNCS11427pp. 262–2782019
  14. A formalization of the LLL basis reduction algorithm ITP 2018LNCS10895pp. 160–1772018
  15. On probabilistic term rewriting FLOPS 2018LNCS10818pp. 132–1482018 [preprint]
  16. Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper) CPP 2018pp. 2–132018
  17. Takashi KitamuraAkihisa YamadaGoro HatayamaShinya SakuragiEun-He ChoiCyrille Artho
    Classification tree method with parameter shielding SAFECOMP 2017LNCS10488pp. 230–2412017
  18. Certifying safety and termination proofs for integer transition systems CADE-26LNCS10395pp. 451–4712017 [preprint]
  19. A formalization of the Berlekamp–Zassenhaus factorization algorithm CPP 2017pp. 17–292017
  20. Distance-integrated combinatorial testing ISSRE 2016pp. 93–1042016 [preprint]
  21. Greedy combinatorial test case generation using unsatisfiable cores ASE 2016pp. 614–6242016 [preprint]
  22. AC dependency pairs revisited CSL 2016LIPIcs62pp. 8:1–8:162016
  23. René ThiemannAkihisa Yamada
    Algebraic numbers in Isabelle/HOL ITP 2016LNCS9807pp. 391–4082016 [preprint]
  24. René ThiemannAkihisa Yamada
    Formalizing Jordan normal forms in Isabelle/HOL CPP 2016pp. 88–99
  25. Takashi KitamuraAkihisa YamadaGoro HatayamaCyrille ArthoEun-He ChoiNgoc Thi Bich DoYutaka OiwaShinya Sakuragi
    Combinatorial testing for tree-structured test models with constraints QRS 2015pp. 141–150 Best paper award! [preprint]
  26. José IborraNaoki NishidaGermán VidalAkihisa Yamada
    Reducing relative termination to dependency pair problems CADE-25LNCS (LNAI)9195pp. 163–178 2015. [preprint, experiments] errata,
  27. Priority integration for weighted combinatorial testing COMPSAC 2015pp. 242–2472015
  28. Optimization of combinatorial testing by incremental SAT solving ICST 2015pp. 1–102015 [preprint]
  29. Nagoya Termination Tool RTA-TLCA 2014LNCS8560pp. 466–4752014 [preprint, full version] errata
  30. AC-KBO revisited FLOPS 2014LNCS8475pp. 319–3352014Superseded by the TPLP article. [preprint, experiments]
  31. Unifying the Knuth-Bendix, recursive path and polynomial orders PPDP 2013pp. 181–1922013 [preprint, experiments]

Theses

Workshop Papers / Others ...

E-mail

akihisa.yamada<at>aist.go.jp