Akihisa Yamada (山田晃久)

Research Interests

Events

Affiliation

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

Tools

I am the developer of and a contributor of

Publications

See also my DBLP entry.

Journal Article

  1. Jose Divasón, Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
    A verified implementation of the Berlekamp–Zassenhaus factorization algorithm. JAR 37 pages, online. [authors' version]
  2. Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
    A verified implementation of algebraic numbers in Isabelle/HOL. JAR 27 pages, online.
  3. José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada:
    Relative termination via dependency pairs. JAR, 58(3):391–411, Springer, 2017. Invited, special issue for CADE 2015.
  4. Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
    AC-KBO revisited. TPLP, 16(2):163–188, Cambridge University Press, 2016. Invited, special issue for FLOPS 2014. Also available as CoRR abs/1403.0406. (errata)
  5. Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
    A unified ordering for termination proving. SCP, 111:110–134, Elsevier, 2015. Invited, special issue for PPDP 2013. Manuscript is available as CoRR abs/1404.6245.
  6. Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, Naoki Nishida:
    A sound type system for typing runtime errors. IPSJ Transactions on Programming, 5(2):16–24, 2012. Awarded IPSJ Tokai-branch student paper prize for encouragement.

Conference Papers

  1. Akihisa Yamada, Jérémy Dubut:
    Complete non-orders and fixed points. ITP 2019. 16 pages, to appear
  2. Dirk Bayer et al.:
    TOOLympics 2019: An overview of competitions in formal methods. TACAS 2019 (3). LNCS 11429, 3–24, 2019.
  3. Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada:
    The termination and complexity competition. TACAS 2019 (3). LNCS 11429, 156–166, 2019.
  4. Christian Sternagel, Akihisa Yamada:
    Reachability analysis for termination and confluence of rewriting. TACAS 2019 (1). LNCS 11427, 262–278, 2019.
  5. Jose Divasón, Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
    A formalization of the LLL basis reduction algorithm. ITP 2018. LNCS 10895, pp. 160–177. 2018
  6. Martin Avanzini, Ugo Dal Lago, Akihisa Yamada:
    On probabilistic term rewriting. FLOPS 2018. LNCS 10818, pp. 132–148, 2018. [preprint]
  7. Jose Divasón, Sebastiaan J.C. Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada:
    Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper). CPP 2018, pp. 2–13, 2018.
  8. Takashi Kitamura, Akihisa Yamada, Goro Hatayama, Shinya Sakuragi, Eun-He Choi, Cyrille Artho:
    Classification tree method with parameter shielding. SAFECOMP 2017. LNCS 10488, pp. 230–241, 2017.
  9. Marc Brockschmidt, Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
    Certifying safety and termination proofs for integer transition systems. CADE-26. LNCS 10395, pp. 451–471, 2017. [preprint]
  10. Jose Divasón, Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
    A formalization of the Berlekamp–Zassenhaus factorization algorithm. CPP 2017. pp. 17–29, 2017.
  11. Eun-He Choi, Cyrille Artho, Takashi Kitamura, Osamu Mizuno, Akihisa Yamada:
    Distance-integrated combinatorial testing. ISSRE 2016. pp. 93–104, 2016. [preprint]
  12. Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, Eun-He Choi:
    Greedy combinatorial test case generation using unsatisfiable cores. ASE 2016. pp. 614–624, 2016. [preprint]
  13. Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari:
    AC dependency pairs revisited. CSL 2016. LIPIcs 62, pp. 8:1–8:16, 2016.
  14. René Thiemann, Akihisa Yamada:
    Algebraic numbers in Isabelle/HOL. ITP 2016. LNCS 9807, pp. 391–408, 2016. [preprint]
  15. René Thiemann, Akihisa Yamada:
    Formalizing Jordan normal forms in Isabelle/HOL. CPP 2016, pp. 88–99.
  16. Takashi Kitamura, Akihisa Yamada, Goro Hatayama, Cyrille Artho, Eun-He Choi, Ngoc Thi Bich Do, Yutaka Oiwa, Shinya Sakuragi:
    Combinatorial testing for tree-structured test models with constraints. QRS 2015, pp. 141–150. Best paper award! [preprint]
  17. José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada:
    Reducing relative termination to dependency pair problems. CADE-25, LNCS (LNAI) 9195, pp. 163–178, 2015. [preprint, experiments] (errata)
  18. Eun-He Choi, Takashi Kitamura, Cyrille Artho, Akihisa Yamada, Yutaka Oiwa:
    Priority integration for weighted combinatorial testing. COMPSAC 2015. pp. 242–247, 2015.
  19. Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-He Choi, Yutaka Oiwa, Armin Biere:
    Optimization of combinatorial testing by incremental SAT solving. ICST 2015, pp. 1–10, 2015. [preprint]
  20. Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
    Nagoya Termination Tool. RTA-TLCA 2014, LNCS 8560, pp. 466–475, 2014. [preprint, full version] (errata)
  21. Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
    AC-KBO revisited. FLOPS 2014, LNCS 8475, pp. 319–335, 2014. Superseded by the TPLP article. [preprint, experiments]
  22. Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
    Unifying the Knuth-Bendix, recursive path and polynomial orders. PPDP 2013, pp. 181–192, 2013. [preprint, experiments]

Theses

Workshop Papers / Others <<<

E-mail

akihisayamada<at>nii.ac.jp