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
Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures.David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL, 2019, Article No.: 29, 1–30. 2019
A Formal Model for Checking Cryptographic API Usage in JavaScript.Duncan Mitchell and Johannes Kinder. In: Sako, K., Schneider, S., Ryan, P. (eds) Computer Security – ESORICS 2019. Lecture Notes in Computer Science, vol 11735. 2019
Program Verification in the Presence of I/O.Hugo Férée, Johannes Å. Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, and Son Ho. In: Piskac, R., Rümmer, P. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2018. Lecture Notes in Computer Science, vol 11294. 2018
Checking cryptographic API usage with composable annotations (short paper).Duncan Mitchell, L. Thomas van Binsbergen, Blake Loring, and Johannes Kinder. PEPM ’18: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, December 2017, 53–59. 2018
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
Blockchain Superoptimizer.Julian Nagele and Maria A Schett. Preproceedings of the 29th International Symposium on Logic-based Program Synthesis and Transformation, LOPSTR 2019, 166-180. 2019
A Key-Value store for Ocaml.Tom Ridge. 24th ACM SIGPLAN International Conference on Functional Programming, ICFP 2019. 2019
PrideMM: A Solver for Relaxed Memory Models.Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, and Mikoláš Janota. arXiv: Logic in Computer Science. 2019