| 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 | 86 | 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 | 36 | 2016 |
| A proof strategy language and proof script generation for Isabelle/HOL Y Nagashima, R Kumar International Conference on Automated Deduction, 528-545, 2017 | 18 | 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 | 13 | 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 | 12 | 2018 |
| 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 | 12 | 2016 |
| Goal-oriented conjecturing for Isabelle/HOL Y Nagashima, J Parsert International Conference on Intelligent Computer Mathematics, 225-231, 2018 | 10 | 2018 |
| LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL Y Nagashima The 17th Asian Symposium on Programming Languages and Systems (APLAS2019), 2019 | 8 | 2019 |
| Towards Evolutionary Theorem Proving for Isabelle/HOL Y Nagashima GECCO2019 Companion (The Genetic and Evolutionary Computation Conference …, 2019 | 4 | 2019 |
| Smart Induction for Isabelle/HOL (Tool Paper) Y Nagashima 2020 Formal Methods in Computer Aided Design (FMCAD), 245-254, 2020 | 2 | 2020 |
| Simple dataset for proof method recommendation in isabelle/hol Y Nagashima International Conference on Intelligent Computer Mathematics, 297-302, 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 |
| Keep failed proof attempts in memory Y Nagashima Isabelle Workshop, Nancy, France, 2016 | 1 | 2016 |
| A proof strategy language and proof script generation for isabelle Y Nagashima, R Kumar CoRR, abs/1606.02941, 2016 | 1 | 2016 |
| SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL Y Nagashima arXiv preprint arXiv:2010.10296, 2020 | | 2020 |
| Faster Smarter Induction in Isabelle/HOL with SeLFiE Y Nagashima arXiv preprint arXiv:2009.09215, 2020 | | 2020 |
| Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description) Y Nagashima arXiv preprint arXiv:2004.10667, 2020 | | 2020 |
| Smart Induction for Isabelle/HOL (System Description) Y Nagashima arXiv preprint arXiv:2001.10834, 2020 | | 2020 |
| Towards United Reasoning for Automatic Induction in Isabelle/HOL Y Nagashima 人工知能学会全国大会論文集 第 34 回全国大会 (2020), 3G1ES103-3G1ES103, 2020 | | 2020 |
| Domain-Specific Language to Encode Induction Heuristics Y Nagashima ICFP 2019 Student Research Competition (arXiv preprint arXiv:1907.02594), 2019 | | 2019 |
Liam O'ConnorUniversity of EdinburghVerified email at ed.ac.uk
