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 | 128 | 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 | 55 | 2016 |
File systems deserve verification too! G Keller, T Murray, S Amani, L O'Connor, Z Chen, L Ryzhyk, G Klein, ... Proceedings of the Seventh Workshop on Programming Languages and Operating …, 2013 | 32 | 2013 |
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 | 26 | 2016 |
Cogent: uniqueness types and certifying compilation L O’CONNOR, Z Chen, C Rizkallah, V Jackson, S Amani, G Klein, ... Journal of Functional Programming 31, e25, 2021 | 19 | 2021 |
Provably trustworthy systems G Klein, J Andronick, G Keller, D Matichuk, T Murray, L O'Connor Philosophical Transactions of the Royal Society A: Mathematical, Physical …, 2017 | 17 | 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 | 15 | 2016 |
The Cogent case for property-based testing Z Chen, L O'Connor, G Keller, G Klein, G Heiser Proceedings of the 9th Workshop on Programming Languages and Operating …, 2017 | 14 | 2017 |
Bringing Effortless Refinement of Data Layouts to Cogent L O’Connor, Z Chen, P Susarla, C Rizkallah, G Klein, G Keller Leveraging Applications of Formal Methods, Verification and Validation …, 2018 | 11 | 2018 |
Type Systems for Systems Types L O'Connor University of New South Wales, 2019 | 10 | 2019 |
Applications of applicative proof search L O'Connor Proceedings of the 1st International Workshop on Type-Driven Development, 43-55, 2016 | 8 | 2016 |
Quickstrom: property-based acceptance testing with LTL specifications L O'Connor, O Wickström Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022 | 5 | 2022 |
Overcoming restraint: composing verification of foreign functions with cogent L Cheung, L O'Connor, C Rizkallah Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022 | 5 | 2022 |
Marginally stable thermal equilibria of Rayleigh-Bénard convection L O'Connor, D Lecoanet, EH Anders Physical Review Fluids 6 (9), 093501, 2021 | 4 | 2021 |
Deferring the details and deriving programs L O'Connor Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven …, 2019 | 3 | 2019 |
Property-Based Testing: Climbing the Stairway to Verification Z Chen, C Rizkallah, L O'Connor, P Susarla, G Klein, G Heiser, G Keller Proceedings of the 15th ACM SIGPLAN International Conference on Software …, 2022 | 2 | 2022 |
Holbert: Reading, Writing, Proving and Learning in the Browser L O'Connor, R Amjad arXiv preprint arXiv:2210.11411, 2022 | 2 | 2022 |
A data layout description language for cogent Z Chen, M Di Meglio, L O’Connor, P Susarla, C Rizkallah, G Keller Proc. PriSC, 1-3, 2019 | 2 | 2019 |
Dargent: A Silver Bullet for Verified Data Layout Refinement Z Chen, A Lafont, L O'Connor, G Keller, C McLaughlin, V Jackson, ... Proceedings of the ACM on Programming Languages 7 (POPL), 1369-1395, 2023 | 1 | 2023 |
Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML Y Nagashima, L O'Connor arXiv preprint arXiv:1608.03350, 2016 | 1 | 2016 |