YAMADA, Akihisa (山田晃久)

Research Interests

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

Affiliation

Tools

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

• IsaFoR/CeTA

Publications

Journal Articles

1. Akihisa Yamada
   Tuple interpretations for termination of term rewriting JARJournal of Automated Reasoning66667–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-IVIEEE Transactions on Intelligent Vehicles843040–30722022
3. Jérémy DubutAkihisa Yamada
   Fixed point theorems for non-transitive relations LMCSLogical Methods in Computer Science18(1:30)2022
4. René ThiemannRalph BotteschJose DivasónMax W. HaslbeckSebastiaan J.C. JoostenAkihisa Yamada
   Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL JARJournal of Automated Reasoning64: 827–856Springer2020 Invited, special issue for ITP 2018. [authors' version]
5. Martin AvanziniUgo Dal LagoAkihisa Yamada
   On probabilistic term rewriting SCPScience of Computer Programming185Elsevier. Invited, special issue for FLOPS 2018, online. [authors' version]
6. Jose DivasónSebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
   A verified implementation of the Berlekamp–Zassenhaus factorization algorithm JARJournal of Automated Reasoning64(4): 699–735Springer2020 [authors' version]
7. Sebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
   A verified implementation of algebraic numbers in Isabelle/HOL JARJournal of Automated Reasoning64:363–389Springer2020
8. José IborraNaoki NishidaGermán VidalAkihisa Yamada
   Relative termination via dependency pairs JARJournal of Automated Reasoning58(3):391–411Springer2017 Invited, special issue for CADE 2015.
9. Akihisa YamadaSarah WinklerNao HirokawaAart Middeldorp
   AC-KBO revisited TPLPTheory and Practice of Logic Programming16(2):163–188Cambridge University Press2016 Invited, special issue for FLOPS 2014. Also available as CoRR abs/1403.0406 errata: In Definition 7.1, "{ t₁,...,t_i-1,s_j,t_i+1,...,t_n }" should be "{ t₁,...,t_i-1 } ⊎ ∇_f (s_j) ⊎ { t_i+1,...,t_n }".
10. Akihisa YamadaKeiichirou KusakariToshiki Sakabe
    A unified ordering for termination proving SCPScience of Computer Programming111:110–134Elsevier2015 Invited, special issue for PPDP 2013. [arXiv version, expreiments].
11. Akihisa YamadaKeiichirou KusakariToshiki SakabeMasahiko SakaiNaoki Nishida
    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

12. Akihisa Yamada
    Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (invited talk) 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)FSCD 2023LIPIcs2604:1–4:52023 [slides]
13. Akihisa YamadaJérémy Dubut
    Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl) 14th International Conference on Interactive Theorem Proving (ITP 2023)ITP 2023LIPIcs268pp. 34:1–34:132023
14. Akihisa Yamada
    Term orderings for non-reachability of (conditional) rewriting Proc. 11th International Joint Conference on Automated Reasoning (IJCAR 2022)IJCAR 2022LNAI13385pp. 248–2672022
15. Akihisa Yamada
    Multi-dimensional interpretations for termination of term rewriting Proc. 28th International Conference on Automated Deduction (CADE-28)CADE-28LNAI12699pp. 273–2902021
16. Clovis EberhartAkihisa YamadaStefan KlikovitsShin'ya KatsumataTsutomu KobayshiIchiro HasuoFuyuki Ishikawa
    Architecture-guided test resource allocation via logic Proc. 15th International Conference on Tests and Proofs (TAP 2021)TAP 2021LNCS12740pp. 22–382021
17. René ThiemannJonas SchöpfChristian SternagelAkihisa Yamada
    Certifying the weighted path order (invited talk) Proc. Joint 5th International Conference on Formal Structures for Computation and Deduction and 10th International Joint Conference on Automatic Reasoning (IJCAR-FSCD 2020)IJCAR-FSCD 2020LIPIcs1674:1–4:202020
18. Juraj KolčákJérémy DubutIchiro HasuoShin'ya KatsumataDavid SprungerAkihisa Yamada
    Relational differential dynamic logic Proc. 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020)TACAS 2020LNCS12078pp. 191–2082020
19. Akihisa YamadaJérémy Dubut
    Complete non-orders and fixed points Proc. 10th International Conference on Interactive Theorem Proving (ITP 2019)ITP 2019LIPIcs14130:1–30:162019
20. 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 Proc. 25th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2019)TACAS 2019 (3)LNCS11429pp. 3–242019
21. Jürgen GieslAlbert RubioChristian SternagelJohannes WaldmannAkihisa Yamada
    The termination and complexity competition Proc. 25th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2019)TACAS 2019 (3)LNCS11429pp. 156–1662019
22. Christian SternagelAkihisa Yamada
    Reachability analysis for termination and confluence of rewriting Proc. 25th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2019)TACAS 2019 (1), LNCS11427pp. 262–2782019
23. Jose DivasónSebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
    A formalization of the LLL basis reduction algorithm Proc. 9th International Conference on Interactive Theorem Proving (ITP 2018)ITP 2018LNCS10895pp. 160–1772018
24. Martin AvanziniUgo Dal LagoAkihisa Yamada
    On probabilistic term rewriting Proc. 14th International Symposium on Functional and Logic Programming (FLOPS 2018)FLOPS 2018LNCS10818pp. 132–1482018 [preprint]
25. Jose DivasónSebastiaan J.C. JoostenOndřej KunčarRené ThiemannAkihisa Yamada
    Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper) Proc. 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018)CPP 2018pp. 2–132018
26. Takashi KitamuraAkihisa YamadaGoro HatayamaShinya SakuragiEun-He ChoiCyrille Artho
    Classification tree method with parameter shielding Proc. 36th International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2017)SAFECOMP 2017LNCS10488pp. 230–2412017
27. Marc BrockschmidtSebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
    Certifying safety and termination proofs for integer transition systems Proc. 26th International Conference on Automated Deduction (CADE-26)CADE-26LNCS10395pp. 451–4712017 [preprint]
28. Jose DivasónSebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
    A formalization of the Berlekamp–Zassenhaus factorization algorithm Proc. 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017)CPP 2017pp. 17–292017
29. Eun-He ChoiCyrille ArthoTakashi KitamuraOsamu MizunoAkihisa Yamada
    Distance-integrated combinatorial testing Proc. 27th International Symposium on Software Reliability Engineering (ISSRE 2016)ISSRE 2016pp. 93–1042016 [preprint]
30. Akihisa YamadaArmin BiereCyrille ArthoTakashi KitamuraEun-He Choi
    Greedy combinatorial test case generation using unsatisfiable cores Proc. 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016)ASE 2016pp. 614–6242016 [preprint]
31. Akihisa YamadaChristian SternagelRené ThiemannKeiichirou Kusakari
    AC dependency pairs revisited Proc. 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)CSL 2016LIPIcs62pp. 8:1–8:162016
32. René ThiemannAkihisa Yamada
    Algebraic numbers in Isabelle/HOL Proc. 7th International Conference on Interactive Theorem Proving (ITP 2016)ITP 2016LNCS9807pp. 391–4082016 [preprint]
33. René ThiemannAkihisa Yamada
    Formalizing Jordan normal forms in Isabelle/HOL Proc. 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016)CPP 2016pp. 88–99
34. Takashi KitamuraAkihisa YamadaGoro HatayamaCyrille ArthoEun-He ChoiNgoc Thi Bich DoYutaka OiwaShinya Sakuragi
    Combinatorial testing for tree-structured test models with constraints Proc. 2015 IEEE International Conference on Software Quality, Reliability & Security (QRS 2015)QRS 2015pp. 141–150 Best paper award! [preprint]
35. José IborraNaoki NishidaGermán VidalAkihisa Yamada
    Reducing relative termination to dependency pair problems Proc. 25th International Conference on Automated Deduction (CADE-25)CADE-25LNCS (LNAI)9195pp. 163–178 2015. [preprint, experiments] errata: In Definition 3, ≻_R/B should be defined as (→_R/B·⊵)⁺, rather than (→_R/B∪⊳)⁺, but then more workaround is required. Please see JAR version for more elegant solution.,
36. Eun-He ChoiTakashi KitamuraCyrille ArthoAkihisa YamadaYutaka Oiwa
    Priority integration for weighted combinatorial testing Proc. 39th Annual International Computers, Software & Applications Conference (COMPSAC 2015)COMPSAC 2015pp. 242–2472015
37. Akihisa YamadaTakashi KitamuraCyrille ArthoEun-He ChoiYutaka OiwaArmin Biere
    Optimization of combinatorial testing by incremental SAT solving Proc. 8th IEEE International Conference on Software Testing, Verification, and Validation (ICST 2015)ICST 2015pp. 1–102015 [preprint]
38. Akihisa YamadaKeiichirou KusakariToshiki Sakabe
    Nagoya Termination Tool Proc. Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014)RTA-TLCA 2014LNCS8560pp. 466–4752014 [preprint, full version] errata: In p.472 line 2, "reset" should be removed from here(); it is not specified in SMT-LIB 2.0, but a command supported by z3.
39. Akihisa YamadaSarah WinklerNao HirokawaAart Middeldorp
    AC-KBO revisited Proc. 12th International Symposium on Functional and Logic Programming (FLOPS 2014)FLOPS 2014LNCS8475pp. 319–3352014Superseded by the TPLP article. [preprint, experiments]
40. Akihisa YamadaKeiichirou KusakariToshiki Sakabe
    Unifying the Knuth-Bendix, recursive path and polynomial orders Proc. 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013)PPDP 2013pp. 181–1922013 [preprint, experiments]

Theses

• The weighted path order for termination of term rewriting Ph.D. thesisGraduate School of Information Science, Nagoya University2014
• An extension of soft typing for static detection of runtime type errors Master's thesisGraduate School of Information Science, Nagoya University2008
• On termination proving of higher order rewrite systems by transformations (in Japanese高階書換え系の変換による停止性証明法に関する研究). Bachelor's thesisSchool of Engineering, Nagoya University2006

Workshop Papers / Others ...

• Juraj KolčákIchiro HasuoJérémy DubutShin'ya KatsumataDavid SprungerAkihisa Yamada
  Relational differential dynamic logic: poster abstract 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2019)HSCC 2019284–2852019
• Akihisa YamadaClovis EberhartFuyuki IshikawaNian-Ze Lee
  Scenario sampling for cyber physical systems using combinatorial testing Poster presentation in 8th International Workshop on Combinatorial Testing (IWCT 2019)IWCT 20192019 [abstract]
• Formalizing cyber physical systems in Isabelle/HOL 若手数学者交流会 2019
• Weighted rewriting 50th TRS meeting 2019 [Slides]
• Relational differential dynamic logic 49th TRS meeting 2018
• Towards unified method for termination 16th International Workshop on Termination (WST 2018)WST 2018pp. 2–62018invited talk
• Jose DivasónSebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
  A Perron-Frobenius theorem for Jordan blocks for complexity proving 16th International Workshop on Termination (WST 2018)WST 2018pp. 30–342018
• Martin AvanziniUgo Dal LagoAkihisa Yamada
  The interpretation method for probabilistic systems 9th International Workshop on Developments in Implicit Computational Complexity (DICE 2018)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 15th International Workshop on Termination (WST 2016)WST 2016p. 25:12016 [slides]
• Sebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
  CeTA – Certifying termination and complexity proofs in 2016 15th International Workshop on Termination (WST 2016)WST 2016p. 20:12016
• Marc BrockschmidtSebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
  Certifying safety and termination proofs for integer transition systems 15th International Workshop on Termination (WST 2016)WST 2016pp. 4:1–4:52016
• Jose DivasónSebastiaan J.C. JoostenOndřej KunčarRené ThiemannAkihisa Yamada
  Certifying exact complexity bounds for matrix interpretations 16th International Workshop on Logic and Computational Complexity (LCC 2016)LCC 2016.
• Jose DivasónSebastiaan J.C. JoostenRené ThiemannAkihisa Yamada
  
  A formalization of Berlekamp's factorization algorithm Isabelle Workshop 2016
• Jose DivasónOndřej KunčarRené ThiemannAkihisa Yamada
  Perron-Frobenius theorem for spectral radius analysis Archive of Formal Proofs2016Formal proof development
• René ThiemannAkihisa Yamada
  Polynomial interpolation Archive of Formal Proofs2016Formal proof development
• René ThiemannAkihisa Yamada
  Polynomial factorization Archive of Formal Proofs2016Formal proof development
• René ThiemannAkihisa Yamada
  Algebraic numbers in Isabelle/HOL Archive of Formal Proofs2015Formal proof development
• René ThiemannAkihisa Yamada
  Matrices, Jordan normal forms, and spectral radius theory Archive of Formal Proofs2015Formal proof development
• Takanori OmaeKeiichirou KusakariAkihisa YamadaToshiki Sakabe
  Abstracting the weighted path order for proving termination of term rewriting systems (in Japanese項書換え系の停止性証明のための重み付き経路順序の抽象化). LA Symposium, 2014 Winter2015
• Koichi OtaTakeshi HamaguchiMasahiko SakaiAkihisa YamadaNaoki NishidaToshiki Sakabe
  Implementing a conditional dependency pair method for proving termination of functional programs with exception handling (in Japanese例外処理を含む関数型プログラムの停止性証明のための条件付き依存対法の実現). IEICE Technical Report SS2014-42Vol. 114, No. 416, pp. 55-602015
• SAT solvers in combinatorial testing 42nd TRS meeting, Tokyo, JapanFebruary2015
• Akihisa YamadaTakashi Kitamura
  Towards developing the combinatorial testing tool Calot (in Japanese組み合わせテストツール Calot の開発に向けて). IPSJ SIGSE Winter Workshop 2015 in Ginowanpp. 53–54January2015
• Eun-He ChoiTakashi KitamuraCyrille ArthoAkihisa YamadaYutaka Oiwa
  T-wise test construction improving (T+1)-way coverage Poster Presentation in 6th International Workshop of Software Engineering in Practice (IWESEP 2014)IWESEP 2014November2014
• SAT solvers and combinatorial testing (in JapaneseSATソルバと組み合わせテスト). Formal Methods Workshop @ IPSJ Software Engineering Symposium (SES 2014), September2014
• Towards dependency pairs for relative termination 40th TRS meeting, Unazuki, JapanMarch2014
• Akihisa YamadaKeiichirou KusakariToshiki Sakabe
  Partial status for KBO Proc. 13th International Workshop on Termination (WST 2013)WST 2013pp. 74–782013 Experiments
• Unifying KBO, LPO and polynomial orders 38th TRS meeting, Kofu, JapanApril2013
• On AC-compatible Knuth-Bendix orderings 37th TRS meeting, Sendai, JapanNovember2012 Joint work with Sarah Winkler, Nao Hirokawa, Aart Middeldorp
• Akihisa YamadaKeiichirou KusakariToshiki SakabeMasahiko SakaiNaoki Nishida
  A sound type system for typing runtime errors 86th Workshop of IPSJ SIGPROYokohama, JapanNovember2011
• Akihisa YamadaKeiichirou KusakariToshiki SakabeMasahiko SakaiNaoki Nishida
  Error detection with soft typing for dynamically typed languages IEICE SIGSSNagasaki, JapanMarch2008

E-mail