Akihisa Yamada (山田晃久)

Research Interests

Interactive Theorem Proving
Combinatorial Testing
Term Rewrite Systems: termination and complexity analysis
Satisfiability

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

the Nagoya Termination Tool, and
the combinatorial testing tool Calot,

and a contributor of

IsaFoR/CeTA.

Publications

Journal Article

Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
A verified implementation of algebraic numbers in Isabelle/HOL. JAR. to appear
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.
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)
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.
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

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
Martin Avanzini, Ugo Dal Lago, Akihisa Yamada:
On probabilistic term rewriting. FLOPS 2018. LNCS 10818, pp. 132–148, 2018.
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.
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.
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.
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.
Eun-He Choi, Cyrille Artho, Takashi Kitamura, Osamu Mizuno, Akihisa Yamada:
Distance-integrated combinatorial testing. ISSRE 2016. pp. 93–104, 2016.
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.
Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari:
AC dependency pairs revisited. CSL 2016. LIPIcs 62, pp. 8:1–8:16, 2016.
René Thiemann, Akihisa Yamada:
Algebraic numbers in Isabelle/HOL. ITP 2016. LNCS 9807, pp. 391–408, 2016.
René Thiemann, Akihisa Yamada:
Formalizing Jordan normal forms in Isabelle/HOL. CPP 2016, pp. 88–99.
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!
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. Experiments (errata)
Eun-He Choi, Takashi Kitamura, Cyrille Artho, Akihisa Yamada, Yutaka Oiwa:
Priority integration for weighted combinatorial testing. COMPSAC 2015. pp. 242–247, 2015.
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.
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
Nagoya Termination Tool. RTA-TLCA 2014, LNCS 8560, pp. 466–475, 2014. Full version appeared as CoRR abs/1404.6626. (errata)
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
AC-KBO revisited. FLOPS 2014, LNCS 8475, pp. 319–335, 2014. Superseded by the TPLP article. Experiments
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
Unifying the Knuth-Bendix, recursive path and polynomial orders. PPDP 2013, pp. 181–192, 2013. Experiments

Theses

The weighted path order for termination of term rewriting. Ph.D. thesis, Graduate School of Information Science, Nagoya University, 2014.
An extension of soft typing for static detection of runtime type errors. Master's thesis, Graduate School of Information Science, Nagoya University, 2008.
On termination proving of higher order rewrite systems by transformations (in Japanese). Bachelor's thesis, School of Engineering, Nagoya University, 2006.

Workshop Papers / Others <<<

Relational differential dynamic logic. 49th TRS meeting. 2018.
Towards unified method for termination. WST 2018, pp. 2–6, 2018. invited talk
Jose Divasón, Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
A Perron-Frobenius theorem for Jordan blocks for complexity proving. WST 2018, pp. 30–34, 2018.
Martin Avanzini, Ugo Dal Lago, Akihisa Yamada:
The interpretation method for probabilistic systems. DICE 2018 @ ETAPS. 2018.
On probabilistic term rewriting. 48th TRS Meeting. 2018.
AC dependency pairs and more. 47th TRS Meeting. 2017.
Isabelle/HOL による証明とプログラミング. PPL サマースクール 2017
Reachability for termination. 4th Austria–Japan Summer Workshop on Term Rewriting (45th TRS meeting). 2016. [slides]
TermComp 2016 participant: NaTT. WST 2016, p. 25:1, 2016.
Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
CeTA – Certifying termination and complexity proofs in 2016. WST 2016, p. 20:1, 2016.
Marc Brockschmidt, Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
Certifying safety and termination proofs for integer transition systems. WST 2016, pp. 4:1–4:5, 2016.
Jose Divasón, Sebastiaan J.C. Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada:
Certifying exact complexity bounds for matrix interpretations. LCC 2016.
Jose Divasón, Sebastiaan J.C. Joosten, René Thiemann, Akihisa Yamada:
A formalization of Berlekamp's factorization algorithm. Isabelle Workshop 2016.
Jose Divasón, Ondřej Kunčar, René Thiemann, Akihisa Yamada:
Perron-Frobenius theorem for spectral radius analysis. Archive of Formal Proofs, 2016 Formal proof development.
René Thiemann, Akihisa Yamada:
Polynomial interpolation. Archive of Formal Proofs, 2016 Formal proof development.
René Thiemann, Akihisa Yamada:
Polynomial factorization. Archive of Formal Proofs, 2016 Formal proof development.
René Thiemann, Akihisa Yamada:
Algebraic numbers in Isabelle/HOL. Archive of Formal Proofs, 2015 Formal proof development.
René Thiemann, Akihisa Yamada:
Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs, 2015 Formal proof development.
Takanori Omae, Keiichirou Kusakari, Akihisa Yamada, Toshiki Sakabe:
Abstracting the weighted path order for proving termination of term rewriting systems (in Japanese). LA Symposium, 2014 Winter, 2015.
Koichi Ota, Takeshi Hamaguchi, Masahiko Sakai, Akihisa Yamada, Naoki Nishida, Toshiki Sakabe:
Implementing a conditional dependency pair method for proving termination of functional programs with exception handling (in Japanese). IEICE Technical Report SS2014-42, Vol. 114, No. 416, pp. 55-60, 2015.
SAT solvers in combinatorial testing. 42nd TRS meeting, Tokyo, Japan, February 2015.
Akihisa Yamada, Takashi Kitamura:
Towards developing the combinatorial testing tool Calot (in Japanese). IPSJ SIGSE Winter Workshop 2015 in Ginowan, pp. 53–54 January 2015.
Eun-He Choi, Takashi Kitamura, Cyrille Artho, Akihisa Yamada, Yutaka Oiwa:
T-wise test construction improving (T+1)-way coverage. Poster Presentation in IWESEP 2014, November 2014.
SAT solvers and combinatorial testing (in Japanese). Formal Methods Workshop @ IPSJ Software Engineering Symposium (SES 2014), September 2014.
Towards dependency pairs for relative termination. 40th TRS meeting, Unazuki, Japan, March 2014.
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe:
Partial status for KBO. WST 2013, pp. 74–78, 2013. Experiments
Unifying KBO, LPO and polynomial orders. 38th TRS meeting, Kofu, Japan, April 2013.
On AC-compatible Knuth-Bendix orderings. 37th TRS meeting, Sendai, Japan, November 2012. Joint work with Sarah Winkler, Nao Hirokawa, Aart Middeldorp
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, Naoki Nishida:
A sound type system for typing runtime errors. 86th Workshop of IPSJ SIGPRO, Yokohama, Japan, November 2011.
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, Naoki Nishida:
Error detection with soft typing for dynamically typed languages. IEICE SIGSS, Nagasaki, Japan, March 2008.

E-mail

akihisayamada<at>nii.ac.jp