Publication

The following is the list of my drafts under review:

• None but I will write a paper about the Abduction Prover in Isabelle/HOL soon.

 

The following is the list of my main publications:

• 2023
  • Template-Based Conjecturing for Automated Induction in Isabelle/HOL
    • Yutaka Nagashima, Zijin Xu, Ningli Wang, Daniel Sebastian Goc, James Bang
    • To appear at FSEN2023 ( formal proceeding / arXiv )
  • Genetic Algorithm for Program Synthesis
    • Yutaka Nagashima
    • To appear at FSEN2023 ( formal proceeding / arXiv )
•  2022
  • Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
    • Yutaka Nagashima
    • I presented this paper at TAP2022 (formal proceeding/arXiv).
•  2021
  • Faster Smarter Induction for Isabelle/HOL
    • Yutaka Nagashima
    • I present this paper at IJCAI2021 (IJCAI proceeding).
    • A promotion video is available at YouTube.
• 2020
  • Smart Induction for Isabelle/HOL (Tool Paper)
    • Yutaka Nagashima
    • The paper is available at TU Wien Academic Press for free.
    • 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
    • Yutaka Nagashima
    • I presented this paper at JSAI2020 (formal proceeding/arXiv).
  • Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
    • Yutaka Nagashima
    • I presented this paper at CICM2020 (arXiv/Springer)
    • The dataset is available at Zenodo.
    • The accompanying Appendix is available at Zenodo.
•  2019
  • LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
    • I presented this paper at APLAS2019 (arXiv/Springer)
    • Yutaka Nagashima
  • Towards Evolutionary Theorem Proving for Isabelle/HOL
    • I presented this poster-only paper at GECCO2019 (arXiv/ACM)
    • Yutaka Nagashima
•  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
    • We presented this paper at CADE2017 (arXiv/Springer).
    • Yutaka Nagashima and Ramana Kumar
• 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
    • I presented this extended abstract at ICFP2019-SRC (arXiv).
    • Yutaka Nagashima
  • Towards Machine Learning Induction
    • I presented this extended abstract at ML2019 (arXiv).
    • I presented this extended abstract at LiVe2019 (arXiv).
    • 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
    • I presented this extended abstract at AITP2018 (informal proceeding).
    • Yutaka Nagashima
• 2017
  • Towards Smart Proof Search for Isabelle
    • I presented this extended abstract at AITP2017 (arXiv).
    • Yutaka Nagashima
• 2016
  • Proof Strategy Language
    • This paper is based on an Isabelle code based published at the Archive of Formal Proofs (AFP).
    • This entry is available here.
    • Yutaka Nagashima
  • 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).