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
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
View-Based Owicki–Gries Reasoning for Persistent x86-TSO. Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, and John Wickerson In: Sergey, I. (eds) Programming Languages and Systems. ESOP 2022. Lecture Notes in Computer Science, vol 13240. 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
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
Static Race Detection and Mutex Safety and Liveness for Go Programs.Julia Gabet and Nobuko Yoshida. 34th European Conference on Object-Oriented Programming, ECOOP 2020. 2020
Learning Weighted Automata over Principal Ideal Domains. FoSSaCS 2020. Lecture Notes in Computer Science, vol 12077.Gerco van Heerdt, Clemens Kupke, Jurriaan Rot, and Alexandra Silva. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. 2020
Modular Relaxed Dependencies in Weak Memory Concurrency.Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, and Mark Batty. In: Müller, P. (eds) Programming Languages and Systems. ESOP 2020. Lecture Notes in Computer Science, vol 12075. 2020
The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation.John Galea and Daniel Kroening. ASIA CCS ’20: Proceedings of the 15th ACM Asia Conference on Computer and Communications Security, October 2020, 622–636. 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
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic.Takamasa Okudono and Andy King. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science, vol 12078. 2020