Publications

2023

  • Hanliang Zhang, Cristina David, Yijun Yu, and Meng Wang. 2023. Ownership Guided C to Rust Translation. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13966. https://doi.org/10.1007/978-3-031-37709-9_22
  • Jerome Jochems, Eddie Jones, and Steven Ramsay. 2023. Higher-order MSL constraints. Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL 2023, Article No.: 69, 2017–2047. https://doi.org/10.1145/3571262
  • Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson. 2023. Taking Back Control in an Intermediate Representation for GPU Computing. Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL 2023, Article No.: 60, 1740–1769. https://doi.org/10.1145/3571253
  • Alastair F. Donaldson, Ben Clayton, Ryan Harrison, Hasan Mohsin, David Neto, Vasyl Teliman, and Hana Watson. 2023. Industrial Deployment of Compiler Fuzzing Techniques for Two GPU Shading Languages. IEEE Conference on Software Testing, Verification and Validation (ICST 2023). http://10.1109/ICST57152.2023.00042
  • Stefan Zetzsche, Alexandra Silva, and Matteo Sammartino. 2023. Guarded Kleene Algebra with Tests: Automata Learning. Electronic Notes in Theoretical Informatics and Computer Science, Volume 1 – Proceedings of MFPS XXXVIII, February 28, 2023, entics:10505. https://doi.org/10.46298/entics.10505
  • Stefan Zetzsche, Alexandra Silva and Matteo Sammartino. 2023. Generators and Bases for Monadic Closures. arXiv: Formal Languages and Automata Theory, 2023.  https://doi.org/10.48550/arXiv.2010.10223
  • Mikhail Semenyuk, Mark Batty and Brijesh Dongol. 2023. Verifying Read-Copy Update Under RC11. In: Ferreira, C., Willemse, T.A.C. (eds) Software Engineering and Formal Methods. SEFM 2023. Lecture Notes in Computer Science, vol 14323. Springer, Cham. https://doi.org/10.1007/978-3-031-47115-5_17
  • Mikhail Semenyuk and Brijesh Dongol. 2023. SAC ’23: Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, March 2023, 1685–1694.  https://doi.org/10.1145/3555776.3577636

2022

  • Zak Cutner, Nobuko Yoshida, and Martin Vassor. 2022. Deadlock-free asynchronous message reordering in Rust with multiparty session types. PPoPP ’2022. https://doi.org/10.48550/arXiv.2112.12693
  • Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, and Idan Refaeli. 2022. Neural Network Robustness as a Verification Property: A Principled Case Study. International Conference on Computer Aided Verification, CAV 2022: Computer Aided Verification, 219–231. https://doi.org/10.1007/978-3-031-13185-1_11
  • Fredrik Dahlqvist  and Renato Neves. 2022. An Internal Language for Categories Enriched over Generalised Metric Spaces. CSL’2022. https://doi.org/10.4230/LIPIcs.CSL.2022.16
  • Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev. 2022. The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency. Proceedings of the ACM on Programming Languages, Volume 6, Issue POPL 2022, Article No.: 54, 1–30. https://doi.org/10.1145/3498716
  • Eddie Jones, C.-H. Luke Ong, and Steven Ramsay. 2022. CycleQ: an efficient basis for cyclic equational reasoning. PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, June 2022, 395–409. https://doi.org/10.1145/3519939.3523731
  • Michalis Pardalos, Yann Herklotz, and John Wickerson. 2022. Resource Sharing for Verified High-Level Synthesis. IEEE 30th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM), 2022, 1-6, https://doi.org/10.1109/FCCM53951.2022.9786208
  • Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. 2022. Modularising Verification Of Durable Opacity. Logical Methods in Computer Science, July 28, 2022, Volume 18, Issue 3. https://doi.org/10.46298/lmcs-18(3:7)2022
  • Wilmer Ricciotti and James Cheney. 2022. A Formalization of SQL with Nulls. Journal of  Automated Reasoning 66, 989–1030, 2022, https://doi.org/10.1007/s10817-022-09632-4
  • Hans-J. Boehm, Ori Lahav, and Azalea Raad. 2022. Foundations of Persistent Programming. DagRep, Volume 11, Issue 10, 2022. https://doi.org/10.4230/DagRep.11.10.94

2021

  • David Kozhaya, Jérémie Decouchant, Vincent Rahli, and Paulo Esteves-Verissimo. 2021. PISTIS: An Event-Triggered Real-Time Byzantine-Resilient Protocol Suite. IEEE Transactions on Parallel and Distributed Systems, vol. 32, no. 9, 2277-2290. https://doi.org/10.1109/TPDS.2021.3056718
  • Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. 2021. Two Mechanisations of WebAssembly 1.0. In Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science, vol 13047. https://doi.org/10.1007/978-3-030-90870-6_4
  • Thomas Bauereiss and Andrei Popescu. 2021. CoSMed: A Confidentiality-Verified Social Media Platform. Arch. Formal Proofs 2021. https://www.isa-afp.org/entries/CoSMed.html
  • Thomas Bauereiss and Andrei Popescu. 2021. CoSMeDis: A Confidentiality-Verified Distributed Social Media Platform. Arch. Formal Proofs 2021. https://www.isa-afp.org/entries/CoSMeDis.html
  • Thomas Bauereiss and Andrei Popescu. 2021. Compositional BD Security. Arch. Formal Proofs 2021. https://www.isa-afp.org/entries/CoSMeDis.html
  • Andrei Popescu, Thomas Bauereiss, and Peter Lammich. 2021. Bounded-Deducibility Security (Invited Paper). Bounded-Deducibility Security (Invited Paper). In L. Cohen, & C. Kaliszyk (Eds.), 12th International Conference on Interactive Theorem Proving, ITP 2021, Italy, 3:1-3:20. https://doi.org/10.4230/LIPIcs.ITP.2021.3
  • Andrei Popescu, Peter Lammich, and Thomas Bauereiss. 2021. CoCon: A Confidentiality-Verified Conference Management System. Arch. Formal Proofs 2021. https://www.isa-afp.org/entries/CoCon.html
  • Eddie Jones and Steven Ramsay. 2021. Intensional datatype refinement: with application to scalable verification of pattern-match safety. Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL, 2021, Article No.: 55, 1–29. https://doi.org/10.1145/3434336
  • Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. 2021. Formal verification of high-level synthesis, Proceedings of the ACM on Programming Languages, Volume 5, Issue OOPSLA, 2021, Article No.: 117, 1–30. https://doi.org/10.1145/3485494
  • Yann Herklotz, Zewei Du, Nadesh Ramanathan, and John Wickerson. 2021. An Empirical Study of the Reliability of High-Level Synthesis Tools. IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM), 2021, 219-223. https://doi.org/10.1109/FCCM51124.2021.00034
  • John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. 2021. Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects of Computing, Volume 33, Issue 4-5, 547–573. https://doi.org/10.1007/s00165-021-00541-8
  • Stefan Zetzsche, Gerco van Heerdt, Matteo Sammartino, and Alexandra Silva. 2021. Canonical Automata via Distributive Law Homomorphisms. EPTCS 351, 2021, 296-313, https://doi.org/10.4204/EPTCS.351.18
  • Matt Windsor, Alastair F. Donaldson, and John Wickerson. 2021. C4: the C compiler concurrency checker. ISSTA 2021: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, July 2021, 670–673, https://dl.acm.org/doi/10.1145/3460319.3469079
  • Wilmer Ricciotti & James Cheney. 2021. Query Lifting: Language-integrated query for heterogeneous nested collections. In: Yoshida, N. (eds) Programming Languages and Systems. ESOP 2021, vol 12648, 579–606. https://doi.org/10.1007/978-3-030-72019-3_21
  • Kristoffer Just Arndal Andersen and Ilya Sergey. 2021. Protocol combinators for modeling, testing, and execution of distributed systems. Journal of Functional Programming, 31, E3, 2021. https://doi:10.1017/S095679682000026X
  • Alastair F. Donaldson, Paul Thomson, Vasyl Teliman, Stefano Milizia, André Perez Maselco, and Antoni Karpiński. 2021. Test-case reduction and deduplication almost for free with transformation-based compiler testing. PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, June 2021, 1017–1032. https://doi.org/10.1145/3453483.3454092

2020

  • Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, and David Aspinall. 2020.  Neural Networks, Secure by Construction. In: Oliveira, B.C.d.S. (eds) Programming Languages and Systems. APLAS 2020, vol 12470. https://doi.org/10.1007/978-3-030-64437-6_4
  • Perdita Stevens. 2020. Connecting software build with maintaining consistency between models: towards sound, optimal, and flexible building from megamodels. Softw Syst Model 19, 935–958, 2020. https://doi.org/10.1007/s10270-020-00788-4
  • Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. 2020. Implementing Multiparty Session Types in Rust. In: Bliudze, S., Bocchi, L. (eds) Coordination Models and Languages. COORDINATION 2020. Lecture Notes in Computer Science, vol 12134. https://doi.org/10.1007/978-3-030-50029-0_8 
  • Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. 2020. Statically verified refinements for multiparty protocols. Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA 2020, Article No.: 148, 1–30. https://doi.org/10.1145/3428216
  • Justus Adam and Stephen Kell. 2020. Type checking beyond type checkers, via slice & run. TAPAS 2020: Proceedings of the 11th ACM SIGPLAN International Workshop on Tools for Automatic Program Analysis, November 2020, 23–29. https://doi.org/10.1145/3427764.3428324
  • Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim. 2020. Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. In: Gotsman, A., Sokolova, A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2020. Lecture Notes in Computer Science, vol 12136. https://doi.org/10.1007/978-3-030-50086-3_3
  • Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance Taylor, Bernardo Toninho, Philip Wadler, and Nobuko Yoshida. 2020. Featherweight go. Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA, 2020, Article No.: 149, 1–29. https://doi.org/10.1145/3428217
  • Julia Gabet and Nobuko Yoshida. 2020. Static Race Detection and Mutex Safety and Liveness for Go Programs. 34th European Conference on Object-Oriented Programming, ECOOP 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.4
  • Gerco van Heerdt, Clemens Kupke, Jurriaan Rot, and Alexandra Silva. 2020. Learning Weighted Automata over Principal Ideal Domains. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science, vol 12077. https://doi.org/10.1007/978-3-030-45231-5_31
  • Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, and Mark Batty. 2020. Modular Relaxed Dependencies in Weak Memory Concurrency. In: Müller, P. (eds) Programming Languages and Systems. ESOP 2020. Lecture Notes in Computer Science, vol 12075. https://doi.org/10.1007/978-3-030-44914-8_22
  • John Galea and Daniel Kroening. 2020. The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation. ASIA CCS ’20: Proceedings of the 15th ACM Asia Conference on Computer and Communications Security, October 2020, 622–636. https://doi.org/10.1145/3320269.3384764
  • Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan. 2020. Proof-Producing Synthesis of CakeML from Monadic HOL Functions. Journal of Automated Reasoning, 64, 1287–1306, 2020. https://doi.org/10.1007/s10817-020-09559-8
  • Takamasa Okudono and Andy King. 2020. Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic. 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. https://doi.org/10.1007/978-3-030-45190-5_5
  • Richard Bornat, Jaap Boender, Florian Kammueller, Guillaume Poly, and Rajagopal Nagarajan. 2020.  Describing and Simulating Concurrent Quantum Systems. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science, vol 12079. https://doi.org/10.1007/978-3-030-45237-7_16
  • Kangfeng Ye, Simon Foster, and Jim Woodcock. 2020. Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP. In: Adamatzky, A., Kendon, V. (eds) From Astrophysics to Unconventional Computation. Emergence, Complexity and Computation, vol 35. https://doi.org/10.1007/978-3-030-15792-0_10
  • Wilmer Ricciotti and James Cheney. 2020. Strongly Normalizing Higher-Order Relational Queries. 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020. https://doi.org/10.4230/LIPIcs.FSCD.2020.28
  • Alastair F. Donaldson, Hugues Evrard, and Paul Thomson. 2020. Putting Randomized Compiler Testing into Production (Experience Report). 34th European Conference on Object-Oriented Programming, ECOOP 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.22

2019

  • David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. 2019. Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL, 2019, Article No.: 29, 1–30. https://doi.org/10.1145/3290342
  • Julian Nagele and Maria A Schett. 2019. Blockchain Superoptimizer. Preproceedings of the 29th International Symposium on Logic-based Program Synthesis and Transformation, LOPSTR 2019, 166-180. https://doi.org/10.48550/arXiv.2005.05912
  • Tom Ridge. 2019. A Key-Value store for Ocaml. 24th ACM SIGPLAN International Conference on Functional Programming, ICFP 2019. https://icfp19.sigplan.org/details/mlfamilyworkshop-2019-papers/10/A-Key-Value-store-for-OCaml
  • Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, and Mikoláš Janota. 2019. PrideMM: A Solver for Relaxed Memory Models. arXiv: Logic in Computer Science. https://doi.org/10.48550/arXiv.1901.00428
  • Nadia Polikarpova and Ilya Sergey. 2019. Structuring the synthesis of heap-manipulating programs. Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL, 2019, Article No.: 72, 1–30. https://doi.org/10.1145/3290385
  • Kristoffer J. A. Andersen and Ilya Sergey. 2019. Distributed Protocol Combinators. In: Alferes, J., Johansson, M. (eds) Practical Aspects of Declarative Languages. PADL 2019. Lecture Notes in Computer Science, vol 11372. https://doi.org/10.1007/978-3-030-05998-9_11
  • Blake Loring, Duncan Mitchell, and Johannes Kinder. 2019. Sound regular expression semantics for dynamic symbolic execution of JavaScript. PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 425–438. https://doi.org/10.1145/3314221.3314645
  • Duncan Mitchell and Johannes Kinder. 2019. A Formal Model for Checking Cryptographic API Usage in JavaScript. In: Sako, K., Schneider, S., Ryan, P. (eds) Computer Security – ESORICS 2019. Lecture Notes in Computer Science, vol 11735. https://doi.org/10.1007/978-3-030-29959-0_17

2018

  • Andrea Giugliano. 2018. Towards verified file systems. PhD Thesis, University of Leicester. https://hdl.handle.net/2381/43220
  • Hugo Férée, Johannes Å. Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, and Son Ho. 2018. Program Verification in the Presence of I/O. In: Piskac, R., Rümmer, P. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2018. Lecture Notes in Computer Science, vol 11294. https://doi.org/10.1007/978-3-030-03592-1_6
  • Duncan Mitchell, L. Thomas van Binsbergen, Blake Loring, and Johannes Kinder. 2018. Checking cryptographic API usage with composable annotations (short paper). PEPM ’18: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, December 2017, 53–59. https://doi.org/10.1145/3162071

2017