| 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 | 64 | 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 | 31 | 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 | 11 | 2016 |
| 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 | 11 | 2016 |
| A proof strategy language and proof script generation for Isabelle/HOL Y Nagashima, R Kumar International Conference on Automated Deduction, 528-545, 2017 | 10 | 2017 |
| PaMpeR: proof method recommendation system for Isabelle/HOL Y Nagashima, Y He ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on …, 2018 | 7 | 2018 |
| Goal-oriented conjecturing for Isabelle/HOL Y Nagashima, J Parsert International Conference on Intelligent Computer Mathematics, 225-231, 2018 | 5 | 2018 |
| LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL Y Nagashima The 17th Asian Symposium on Programming Languages and Systems (APLAS2019), 2019 | 2 | 2019 |
| Towards Evolutionary Theorem Proving for Isabelle/HOL Y Nagashima GECCO2019 Companion (The Genetic and Evolutionary Computation Conference …, 2019 | 1 | 2019 |
| 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 arXiv preprint arXiv:1606.02941, 2016 | 1 | 2016 |
| Smart Induction for Isabelle/HOL (System Description) Y Nagashima arXiv preprint arXiv:2001.10834, 2020 | | 2020 |
| Domain-Specific Language to Encode Induction Heuristics Y Nagashima ICFP 2019 Student Research Competition (arXiv preprint arXiv:1907.02594), 2019 | | 2019 |
| Designing Game of Theorems Y Nagashima Conference on Artificial Intelligence and Theorem Proving (AITP2018) (arXiv …, 2019 | | 2019 |
| Towards Machine Learning Induction Y Nagashima AITP2019; LiVe2019; arXiv preprint arXiv:1812.04088, 2018 | | 2018 |
| Designing Games of Theorem Proving Y Nagashima AITP 2018, 2018 | | 2018 |
| Towards Smart Proof Search for Isabelle Y Nagashima AITP2017; arXiv preprint arXiv:1701.03037, 2017 | | 2017 |
| The Diameter of Binary Multithreaded Programs A Malkis, Y Nagashima, S Borgwardt, C Eckert | | 2013 |
| The Diameter of Multithreaded Programs: Preliminary Findings S Borgwardt, A Malkis, Y Nagashima | | |
Toby MurraySchool of Computing and Information Systems, University of MelbourneVerified email at unimelb.edu.au
