| Cogent: Verifying high-assurance file system implementations S Amani, A Hixon, Z Chen, C Rizkallah, P Chubb, L O'Connor, J Beeren, ... ACM SIGARCH Computer Architecture News 44 (2), 175-188, 2016 | 137 | 2016 |
| Refinement through restraint: Bringing down the cost of verification L O'Connor, Z Chen, C Rizkallah, S Amani, J Lim, T Murray, Y Nagashima, ... ACM SIGPLAN Notices 51 (9), 89-102, 2016 | 60 | 2016 |
| A Framework for the Automatic Formal Verification of Refinement from Cogent to C C Rizkallah, J Lim, Y Nagashima, T Sewell, Z Chen, L O’Connor, T Murray, ... International Conference on Interactive Theorem Proving, 323-340, 2016 | 31 | 2016 |
| PaMpeR: proof method recommendation system for Isabelle/HOL Y Nagashima, Y He ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on …, 2018 | 30 | 2018 |
| A proof strategy language and proof script generation for Isabelle/HOL Y Nagashima, R Kumar Automated Deduction–CADE 26: 26th International Conference on Automated …, 2017 | 29 | 2017 |
| COGENT: certified compilation for a functional systems language L O'Connor, C Rizkallah, Z Chen, S Amani, J Lim, Y Nagashima, T Sewell, ... arXiv preprint arXiv:1601.05520, 2016 | 18 | 2016 |
| LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL Y Nagashima The 17th Asian Symposium on Programming Languages and Systems (APLAS2019), 2019 | 16 | 2019 |
| Goal-oriented conjecturing for Isabelle/HOL Y Nagashima, J Parsert Intelligent Computer Mathematics: 11th International Conference, CICM 2018 …, 2018 | 15 | 2018 |
| Towards Evolutionary Theorem Proving for Isabelle/HOL Y Nagashima GECCO2019 Companion (The Genetic and Evolutionary Computation Conference …, 2019 | 11 | 2019 |
| Simple dataset for proof method recommendation in isabelle/hol Y Nagashima International Conference on Intelligent Computer Mathematics, 297-302, 2020 | 7 | 2020 |
| Smart induction for Isabelle/HOL (tool paper) Y Nagashima # PLACEHOLDER_PARENT_METADATA_VALUE# 1, 245-254, 2020 | 7 | 2020 |
| Faster Smarter Proof by Induction in Isabelle/HOL. Y Nagashima IJCAI, 1981-1988, 2021 | 6 | 2021 |
| SeLFiE: Modular semantic reasoning for induction in Isabelle/HOL Y Nagashima CoRR, abs/2010.10296, 2020 | 3 | 2020 |
| Template-Based Conjecturing for Automated Induction in Isabelle/HOL Y Nagashima, Z Xu, N Wang, DS Goc, J Bang International Conference on Fundamentals of Software Engineering, 112-125, 2023 | 2 | 2023 |
| Definitional quantifiers realise semantic reasoning for proof by induction Y Nagashima International Conference on Tests and Proofs, 48-66, 2022 | 2 | 2022 |
| Property-based conjecturing for automated induction in Isabelle/HOL Y Nagashima, Z Xu, N Wang, DS Goc, J Bang CoRR, abs/2212.11151, 2022 | 2 | 2022 |
| Genetic Algorithm for Program Synthesis Y Nagashima International Conference on Fundamentals of Software Engineering, 104-111, 2023 | 1 | 2023 |
| Towards united reasoning for automatic induction in Isabelle/HOL Y Nagashima arXiv preprint arXiv:2005.12737, 2020 | 1 | 2020 |
| Simple dataset for proof method recommendation in Isabelle/HOL (dataset description) Y Nagashima arXiv preprint arXiv:2004.10667, 2020 | 1 | 2020 |
| Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML Y Nagashima, L O'Connor ML2016; arXiv preprint arXiv:1608.03350, 2016 | 1 | 2016 |
Liam O'ConnorThe Australian National University and The University of EdinburghVerified email at anu.edu.au
