Gregersen, S. O.
, Aguirre, A., Haselwarter, P. G., Tassarotti, J.
& Birkedal, L. (2024).
Almost-Sure Termination by Guarded Refinement.
Proceedings of the ACM on Programming Languages ,
8(ICFP), 203-233. Artikel 243.
https://doi.org/10.1145/3674632
Hammond, A.
, Liu, Z., Pérami, T., Sewell, P.
, Birkedal, L. & Pichon-Pharabod, J. (2024).
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.
Proceedings of the ACM on Programming Languages ,
8, 604-637. Artikel 21.
https://doi.org/10.1145/3632863
Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J.
& Birkedal, L. (2024).
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
Proceedings of the ACM on Programming Languages ,
8(POPL), Artikel 26.
https://doi.org/10.1145/3632868
Georges, A. L., Guéneau, A., Van Strydonck, T.
, Timany, A., Trieu, A., Devriese, D.
& Birkedal, L. (2024).
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.
Journal of the ACM,
71(1), Artikel 3.
https://doi.org/10.1145/3623510
Aguirre, A., Haselwarter, P. G., De Medeiros, M.
, Li, K. H., Gregersen, S. O., Tassarotti, J.
& Birkedal, L. (2024).
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.
Proceedings of the ACM on Programming Languages ,
8, Artikel 246.
https://doi.org/10.1145/3674635
Legoupil, M., Rousseau, J., Georges, A. L.
, Pichon-Pharabod, J. & Birkedal, L. (2024).
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly.
Proceedings of the ACM on Programming Languages ,
8(OOPSLA2), Artikel 282.
https://doi.org/10.1145/3689722
Dahlsen-Jensen, M. B., Fievet, B., Petrucci, L.
& de Pol, J. V. (2024).
On-The-Fly Algorithm for Reachability in Parametric Timed Games. I B. Finkbeiner & L. Kovács (red.),
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings (s. 194-212). Springer Science and Business Media Deutschland GmbH.
https://doi.org/10.1007/978-3-031-57256-2_10
Haselwarter, P. G., Li, K. H. E. I., Medeiros, M. D. E.
, Gregersen, S. O., Aguirre, A., Tassarotti, J.
& Birkedal, L. (2024).
Tachis: Higher-Order Separation Logic with Credits for Expected Costs.
Proceedings of the ACM on Programming Languages ,
8(OOPSLA2), 1189 - 1218. Artikel 313.
https://doi.org/10.1145/3689753
Haselwarter, P. G., Hvass, B. S., Hansen, L. L., Winterhalter, T., Hriţcu, C.
& Spitters, B. (2024).
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. I A. Timany, D. Traytel, B. Pientka & S. Blazy (red.),
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (s. 30-44). Association for Computing Machinery.
https://doi.org/10.1145/3636501.3636961
Timany, A., Gregersen, S. O., Stefanesco, L.
, Hinrichsen, J. K., Gondelman, L., Nieto, A.
& Birkedal, L. (2024).
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement.
Proceedings of the ACM on Programming Languages ,
8, Artikel 9.
https://doi.org/10.1145/3632851
Pientka, B., Blazy, S., Traytel, D.
& Timany, A. (2024).
Welcome from the Chairs. I
CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024 (s. iii-iv)
Sølvsten, S. & van de Pol, J. (2023).
Adiar 1.1: Zero-Suppressed Decision Diagrams in External Memory. I K. Y. Rozier & S. Chaudhuri (red.),
NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings (s. 464-471). Springer.
https://doi.org/10.1007/978-3-031-33170-1_28
Larsen, C. A., Schmidt, S. M., Steensgaard, J., Jakobsen, A. B., Pol, J. V. D. & Pavlogiannis, A. (2023).
A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. I S. Sankaranarayanan & N. Sharygina (red.),
Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II (s. 353-371). Springer.
https://doi.org/10.1007/978-3-031-30820-8_22
Rao, X.
, Georges, A. L., Legoupil, M., Watt, C.
, Pichon-Pharabod, J., Gardner, P.
& Birkedal, L. (2023).
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs.
Proceedings of the ACM on Programming Languages ,
7, Artikel 151.
https://doi.org/10.1145/3591265
Guéneau, A., Hostert, J., Spies, S., Sammler, M.
, Birkedal, L. & Dreyer, D. (2023).
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C.
Proceedings of the ACM on Programming Languages ,
7(OOPSLA2), 716-744. Artikel 247.
https://doi.org/10.1145/3622823
Nieto, A., Daby-Seesaram, A.
, Gondelman, L., Timany, A. & Birkedal, L. (2023).
Modular Verification of State-Based CRDTs in Separation Logic. I K. Ali & G. Salvaneschi (red.),
37th European Conference on Object-Oriented Programming, ECOOP 2023 Artikel 22 Dagstuhl Publishing.
https://doi.org/10.4230/LIPIcs.ECOOP.2023.22
Haselwarter, P. G., Rivas, E., Van Muylder, A., Winterhalter, T., Abate, C.
, Sidorenco, N., Hriţcu, C., Maillard, K.
& Spitters, B. (2023).
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
ACM Transactions on Programming Languages and Systems,
45(3), 61. Artikel 15.
https://doi.org/10.1145/3594735
Gondelman, L., Hinrichsen, J. K., Pereira, M.
, Timany, A. & Birkedal, L. (2023).
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols.
Proceedings of the ACM on Programming Languages ,
7(ICFP), 847-877. Artikel 217.
https://doi.org/10.1145/3607859
Liu, Z., Stepanenko, S., Pichon-Pharabod, J., Timany, A., Askarov, A. & Birkedal, L. (2023).
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.
Proceedings of the ACM on Programming Languages ,
7, 1438-1462.
https://doi.org/10.1145/3591279
Sølvsten, S. C., de Pol, J. V., Jakobsen, A. B. & Thomasen, M. W. B. (2022).
Adiar Binary Decision Diagrams in External Memory. I D. Fisman & G. Rosu (red.),
Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings (s. 295-313). Springer.
https://doi.org/10.1007/978-3-030-99527-0_16
Bloemen, V., Zelst, S. V., Aalst, W. V. D., Dongen, B. V.
& Pol, J. V. D. (2022).
Aligning observed and modelled behaviour by maximizing synchronous moves and using milestones.
Information Systems,
103, Artikel 101456.
https://doi.org/10.1016/j.is.2019.101456