Publication

The following is the list of my drafts:

  • 2020
    • SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL
      • The draft is available at arXiv.
      • This draft is under review at APLAS2021.

The following is the list of my main publications:

  • 2021
  • 2020
    • Smart Induction for Isabelle/HOL (Tool Paper)
      • Yutaka Nagashima
      • The draft is available at Zenodo.
      • I presented this paper at FMCAD2020.
      • A promotion video is available for this paper at YouTube.
    • Towards United Reasoning for Automatic Induction in Isabelle/HOL
    • Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
  •  2019
    • LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
    • Towards Evolutionary Theorem Proving for Isabelle/HOL
  •  2018
    • Goal-Oriented Conjecturing for Isabelle/HOL
      • We presented this paper at CICM2018 (arXiv/Springer).
      • Yutaka Nagashima and Julian Parsert
      • This paper won the best system award.
    • PaMpeR: Proof Method Recommendation System for Isabelle/HOL
      • We presented this paper at ASE2018 (arXiv/ACM).
      • Yutaka Nagashima and Yilun He
  • 2017
    • A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
  • 2016
    • Refinement through Restraint: Bringing Down the Cost of Verification
      • We presented this paper at ICFP2016 (Data61/SIGPLAN).
      • Liam O’Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
    • A framework for the automatic formal verification of refinement from Cogent to C
      • We presented this paper at ITP2016 (Data61/Springer).
      • Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O’Connor, Toby Murray, Gabriele Keller and Gerwin Klein
    • Cogent: Verifying High-Assurance File System Implementations
      • We presented this paper at ASPLOS2016 (Data61/ACM).
      • Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser

The following is the list of my extended abstracts, minor publications, and informal workshop talks without formal proceedings:

  • 2020
    • Smart Induction for Isabelle/HOL (Tool Paper)
      • Yutaka Nagashima
      • The draft is available at Zenodo.
      • I presented this paper at Isabelle2020.
    • LiFtEr: Language to Encode Induction Heuristics
      • I presented this extended abstract at AITP2020 .
      • Yutaka Nagashima
  •  2019
    • Towards United Reasoning for Automatic Induction in Isabelle/HOL
      • I presented this extended abstract during the poster session at APLAS2019.
      • Yutaka Nagashima
      • This poster presentation was short listed for the best poster award.
    • Domain-Specific Language to Encode Induction Heuristics
    • Towards Machine Learning Induction
      • I presented this extended abstract at AITP2019 (arXiv).
      • Yutaka Nagashima
  • 2018
    • PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
      • We presented this paper at Isabelle2018.
      • Yutaka Nagashima and Yilun He
    • Designing Games of Theorem Proving
  • 2017
    • Towards Smart Proof Search for Isabelle
      • I presented this extended abstract at AITP2017 (arXiv).
      • Yutaka Nagashima
  • 2016
    • Proof Strategy Language
    • Close Encounters of the Higher Kind – Emulating Constructor Classes in Standard ML (extended abstract)
      • We presented this extended abstract at ML2016 (arXiv/YouTube).
      • Yutaka Nagashima and Liam O’Connor
    • Keep Failed Proof Attempts in Memory
      • We presented this paper at Isabelle2016 (Data61).