Deadlock-free asynchronous message reordering in Rust with multiparty session types.Zak Cutner, Nobuko Yoshida, and Martin Vassor. PPoPP ’2022. 2022
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
An Internal Language for Categories Enriched over Generalised Metric Spaces.Fredrik Dahlqvist and Renato Neves. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 16:1-16:18 2022
The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency.Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev. Proceedings of the ACM on Programming Languages, Volume 6, Issue POPL 2022, Article No.: 54, 1–30. 2022
CycleQ: an efficient basis for cyclic equational reasoning.Eddie Jones, C.-H. Luke Ong, and Steven Ramsay. PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language, Pages 395–409. 2022
Resource Sharing for Verified High-Level Synthesis.Michalis Pardalos, Yann Herklotz, and John Wickerson. IEEE 30th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM), 2022, 1-6. 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
C4: the C compiler concurrency checker.Matt Windsor, Alastair F. Donaldson, and John Wickerson. ISSTA 2021: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, July 2021, 670–673. 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
Query Lifting: Language-integrated query for heterogeneous nested collections.Wilmer Ricciotti & James Cheney. In: Yoshida, N. (eds) Programming Languages and Systems. ESOP 2021, vol 12648, 579–606. 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
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
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
CoCon: A Confidentiality-Verified Conference Management System.Andrei Popescu, Peter Lammich, and Thomas Bauereiss. Arch. Formal Proofs 2021. 2021