Two Mechanisations of WebAssembly 1.0.Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. In Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science, vol 13047. 2021
Bounded-Deducibility Security (Invited Paper).Andrei Popescu, Thomas Bauereiss, and Peter Lammich. In L. Cohen, & C. Kaliszyk (Eds.), 12th International Conference on Interactive Theorem Proving, ITP 2021, Italy, 3:1-3:20. 2021
Intensional datatype refinement: with application to scalable verification of pattern-match safety.Eddie Jones and Steven Ramsay. Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL, 2021, Article No.: 55, 1–29. 2021
Formal verification of high-level synthesis.Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Proceedings of the ACM on Programming Languages, Volume 5, Issue OOPSLA, 2021, Article No.: 117, 1–30. 2021
An Empirical Study of the Reliability of High-Level Synthesis Tools.Yann Herklotz, Zewei Du, Nadesh Ramanathan, and John Wickerson. IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM), 2021, 219-223. 2021
Modularising Verification Of Durable Opacity.Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Logical Methods in Computer Science, July 28, 2022, Volume 18, Issue 3. 2022
Verifying correctness of persistent concurrent data structures: a sound and complete method.John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Formal Aspects of Computing, Volume 33, Issue 4-5, 547–573. 2021
Ownership-Based Owicki-Gries Reasoning.Mikhail Semenyuk and Brijesh Dongol. SAC ’23: Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, March 2023, 1685–1694. 2023
Canonical Algebraic Generators in Automata LearningStefan Jens Zetzsche. PhD Thesis, University College London. 2023
Specifying and Verifying Persistent Transactional MemoryEleni Vafeiadi Bila. PhD Thesis, University of Surrey. 2023
Verified compilation of a purely functional language to a realistic machine semanticsHrutvik Kanabar. PhD Thesis, University of Kent. 2023
Lightweight Approaches to the Verification of Functional Programs.Eddie Jones. PhD Thesis, University of Bristol. 2023
Ownership Guided C to Rust Translation.Hanliang Zhang, Cristina David, Yijun Yu, and Meng Wang. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13966. 2023
Deadlock-free asynchronous message reordering in Rust with multiparty session types.Zak Cutner, Nobuko Yoshida, and Martin Vassor. PPoPP ’2022. 2022
Higher-order MSL constraints.Jerome Jochems, Eddie Jones, and Steven Ramsay. Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL 2023, Article No.: 69, 2017–2047. 2023
Neural Network Robustness as a Verification Property: A Principled Case Study.Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, and Idan Refaeli. International Conference on Computer Aided Verification, CAV 2022: Computer Aided Verification, 219–231. 2022