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
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
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
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
Sound regular expression semantics for dynamic symbolic execution of JavaScript.Blake Loring, Duncan Mitchell, and Johannes Kinder. PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 425–438. 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
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