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
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
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
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
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
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
A Key-Value store for Ocaml.Tom Ridge. 24th ACM SIGPLAN International Conference on Functional Programming, ICFP 2019. 2019
PrideMM: A Solver for Relaxed Memory Models.Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, and Mikoláš Janota. arXiv: Logic in Computer Science. 2019
Structuring the synthesis of heap-manipulating programs.Nadia Polikarpova and Ilya Sergey. Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL, 2019, Article No.: 72, 1–30. 2019