Mehnert, H.
, Sieczkowski, F., Birkedal, L. & Sestoft, P. (2012).
Formalized verification of snapshotable trees: Separation and sharing. In R. Joshi, P. Müller & A. Podelski (Eds.),
Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings (pp. 179-195). Springer.
https://doi.org/10.1007/978-3-642-27705-4_15
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
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. In S. Sankaranarayanan & N. Sharygina (Eds.),
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 (pp. 353-371). Springer.
https://doi.org/10.1007/978-3-031-30820-8_22
Krogh-Jespersen, M.
, Timany, A., Ohlenbusch, M. E.
, Gregersen, S. O. & Birkedal, L. (2020).
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In P. Müller (Ed.),
Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings (pp. 336-365). Springer.
https://doi.org/10.1007/978-3-030-44914-8_13
Krishnaswami, N. R., Aldrich, J.
, Birkedal, L., Svendsen, K. & Buisse, A. (2009).
Design patterns in separation logic. In A. Kennedy & A. Ahmed (Eds.),
Proceedings of the 2009 ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI'09 (pp. 105-115). Association for Computing Machinery.
https://doi.org/10.1145/1481861.1481874
Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D.
& Birkedal, L. (2017).
The Essence of Higher-Order Concurrent Separation Logic. In H. Yang (Ed.),
Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings (pp. 696-723). Springer VS.
https://doi.org/10.1007/978-3-662-54434-1_26
Krebbers, R.
, Timany, A. & Birkedal, L. (2017).
Interactive proofs in higher-order concurrent separation logic. In A. D. Gordon & G. Castagna (Eds.),
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 (pp. 205-217). Association for Computing Machinery.
https://doi.org/10.1145/3009837.3009855
Krebbers, R., Jourdan, J.-H., Jung, R., Tassarotti, J., Kaiser, J.-O.
, Timany, A., Charguéraud, A. & Dreyer, D. (2018).
MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
PACMPL,
2(ICFP), 77:1-77:30. Article 3236772.
https://doi.org/10.1145/3236772
Khurana, S., Schivo, S., Plass, J. R. M., Mersinis, N., Scholma, J., Kerkhofs, J., Zhong, L.
, van de Pol, J., Langerak, R., Geris, L., Karperien, M. & Post, J. N. (2021).
An ECHO of Cartilage: In Silico Prediction of Combinatorial Treatments to Switch Between Transient and Permanent Cartilage Phenotypes With Ex Vivo Validation.
Frontiers in Bioengineering and Biotechnology,
9, Article 732917.
https://doi.org/10.3389/fbioe.2021.732917
Karbyshev, A., Svendsen, K.
, Askarov, A. & Birkedal, L. (2018).
Compositional Non-interference for Concurrent Programs via Separation and Framing. In L. Bauer & R. Küsters (Eds.),
Principles of Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (Vol. 10804, pp. 53-78). Springer VS.
https://doi.org/10.1007/978-3-319-89722-6_3
JUNG, RALF., KREBBERS, ROBBERT., JOURDAN, JACQUES.-HENRI., BIZJAK, ALEŠ.
, BIRKEDAL, LARS. & DREYER, DEREK. (2018).
Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
Journal of Functional Programming,
28, 1-73. Article e20.
https://doi.org/10.1017/S0956796818000151
Jung, R., Swasey, D.
, Sieczkowski, F., Svendsen, K., Turon, A.
, Birkedal, L. & Dreyer, D. (2015).
Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In S. Rajamani (Ed.),
Conference Record of the Annual ACM Symposium on Principles of Programming Languages (pp. 637-650). Association for Computing Machinery.
https://doi.org/10.1145/2676726.2676980
Jung, R., Lepigre, R., Parthasarathy, G., Rapoport, M.
, Timany, A., Dreyer, D. & Jacobs, B. (2020).
The future is ours: prophecy variables in separation logic.
Proceedings of the ACM on Programming Languages ,
4(POPL), Article 45.
https://doi.org/10.1145/3371113
Jensen, J. B.
& Birkedal, L. (2012).
Fictional Separation Logic. In H. Seidl (Ed.),
Lecture Notes in Computer Science: 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings (Vol. 7211, pp. 377-396). Springer.
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. Article 15.
https://doi.org/10.1145/3594735
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. In A. Timany, D. Traytel, B. Pientka & S. Blazy (Eds.),
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 30-44). Association for Computing Machinery.
https://doi.org/10.1145/3636501.3636961
Hansen, S. T., Gomes, C., Palmieri, M., Thule, C.
, van de Pol, J. & Woodcock, J. (2021).
Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps. In A. L. Lafuente & A. Mavridou (Eds.),
Formal Methods for Industrial Critical Systems (pp. 3-20). Springer.
https://doi.org/10.1007/978-3-030-85248-1_1