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
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
A Formalization of SQL with Nulls.Wilmer Ricciotti and James Cheney. Journal of Automated Reasoning 66, 989–1030. 2022
PISTIS: An Event-Triggered Real-Time Byzantine-Resilient Protocol Suite.David Kozhaya, Jérémie Decouchant, Vincent Rahli, and Paulo Esteves-Verissimo. IEEE Transactions on Parallel and Distributed Systems, vol. 32, no. 9, 2277-2290. 2021
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
Protocol combinators for modeling, testing, and execution of distributed systems.Kristoffer Just Arndal Andersen and Ilya Sergey. Journal of Functional Programming, 31, E3, 2021. 2021
Proof-Producing Synthesis of CakeML from Monadic HOL Functions. Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan. Journal of Automated Reasoning, 64, 1287–1306, 2020. 2020
Connecting software build with maintaining consistency between models: towards sound, optimal, and flexible building from megamodels.Perdita Stevens. Softw Syst Model 19, 935–958, 2020. 2020
Logic in Computer ScienceOn the Quest for an Acyclic Graph.Mikolas Janota, Radu Grigore, and Vasco Manquinho. arXiv: Logic in Computer Science. 2017
ExpoSE: practical symbolic execution of standalone JavaScript.Blake Loring, Duncan Mitchell, and Johannes Kinder. SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, July 2017, 196–199. 2017
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures.Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, Azalea Raad. Proceedings of the ACM on Programming Languages, Volume 8, Issue OOPSLA2 Article No.: 341, Pages 1982 – 2009. OOPSLA 2024.