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 [...]
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
Compositional BD Security.
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. [...]
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 [...]
Ownership Guided C to Rust Translation.
Hanliang Zhang, Cristina David, Yijun Yu, and Meng Wang. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, [...]
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. [...]
Higher-order MSL constraints.
Jerome Jochems, Eddie Jones, and Steven Ramsay. Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL 2023, Article No.: 69, 2017–2047. 2023
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, [...]
by