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
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
Canonical Automata via Distributive Law Homomorphisms.Stefan Zetzsche, Gerco van Heerdt, Matteo Sammartino, and Alexandra Silva. EPTCS 351, 2021, 296-313. 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
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
Foundations of Persistent Programming.Hans-J. Boehm, Ori Lahav, and Azalea Raad. In Dagstuhl Reports, Volume 11, Issue 10, pp. 94-110, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) 2022
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
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
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
CoCon: A Confidentiality-Verified Conference Management System.Andrei Popescu, Peter Lammich, and Thomas Bauereiss. Arch. Formal Proofs 2021. 2021
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
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