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
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
CoSMed: A Confidentiality-Verified Social Media Platform.Thomas Bauereiss and Andrei Popescu. Arch. Formal Proofs 2021. 2021
CoSMeDis: A Confidentiality-Verified Distributed Social Media Platform.Thomas Bauereiss and Andrei Popescu. Arch. Formal Proofs 2021. 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
CoCon: A Confidentiality-Verified Conference Management System.Andrei Popescu, Peter Lammich, and Thomas Bauereiss. Arch. Formal Proofs 2021. 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
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
Test-case reduction and deduplication almost for free with transformation-based compiler testing.Alastair F. Donaldson, Paul Thomson, Vasyl Teliman, Stefano Milizia, André Perez Maselco, and Antoni Karpiński. PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, June 2021, 1017–1032. 2021
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
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