Publications

Sort by: Date | Author | Title

Wimmer, S., Herbreteau, F. & van de Pol, J. (2020). Certifying Emptiness of Timed Büchi Automata. In N. Bertrand & N. Jansen (Eds.), Formal Modeling and Analysis of Timed Systems : 18th International Conference, FORMATS 2020 (pp. 58-75). Springer. https://doi.org/10.1007/978-3-030-57628-8_4

Vindum, S. F. & Birkedal, L. (2021). Contextual refinement of the Michael-Scott queue (proof pearl). In C. Hriţcu & A. Popescu (Eds.), CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 76-90). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439930

Vindum, S. F., Frumin, D. & Birkedal, L. (2022). Mechanized Verification of a Fine-Grained Concurrent Queue from Meta s Folly Library. In A. Popescu & S. Zdancewic (Eds.), CPP 2022 : Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022 (pp. 100-115). Association for Computing Machinery. https://doi.org/10.1145/3497775.3503689

Vindum, S. F. & Birkedal, L. (2023). Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory. Proceedings of the ACM on Programming Languages , 7(OOPSLA2), 632-657. Article 244. https://doi.org/10.1145/3622820

Vindum, S. F., Georges, A. L. & Birkedal, L. (2025). The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. In K. Stark, A. Timany, S. Blazy & N. Tabareau (Eds.), Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2025 (pp. 83-97). Association for Computing Machinery. https://doi.org/10.1145/3703595.3705876

Veileborg, O. H., Saioc, G.-V. & Møller, A. (2022). Detecting Blocking Errors in Go Programs using Localized Abstract Interpretation. In iWOAR 2022 - 7th International Workshop on Sensor-Based Activity Recognition and Artificial Intelligence, Proceedings (pp. 1-12). Article 32 Association for Computing Machinery. https://doi.org/10.1145/3551349.3561154

Varming, C. & Birkedal, L. (2008). Higher-Order Separation Logic in Isabelle/HOLCF. Electronic Notes in Theoretical Computer Science, 218, 371-389. https://doi.org/10.1016/j.entcs.2008.10.022

Van Der Berg, F. I. & Van De Pol, J. (2019). Concurrent chaining hash maps for software model checking. In C. Barrett & J. Yang (Eds.), Proceedings of the 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019 (pp. 46-54). Article 8894279 IEEE. https://doi.org/10.23919/FMCAD.2019.8894279

van de Pol, J. (2019). Concurrent algorithms and data structures for model checking. In W. Fokkink & R. van Glabbeek (Eds.), 30th International Conference on Concurrency Theory, CONCUR 2019 Article 4 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2019.4

van de Pol, J. (2022). Exploring a Parallel SCC Algorithm: Using TLA ⁺ and the TLC Model Checker. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings (pp. 535-555). Springer. https://doi.org/10.1007/978-3-031-19849-6_30

van de Pol, J. & Petrucci, L. (2021). On Completeness of Liveness Synthesis for Parametric Timed Automata (Extended Abstract). In M. Roggenbach (Ed.), Recent Trends in Algebraic Development Techniques - 25th International Workshop, WADT 2020, Revised Selected Papers (pp. 3-10). Springer Science+Business Media. https://doi.org/10.1007/978-3-030-73785-6_1

van de Pol, J. & Bouyer, P. (Eds.) (2025). 36th International Conference on Concurrency Theory, CONCUR 2025. Dagstuhl Publishing. Leibniz International Proceedings in Informatics, LIPIcs Vol. 348 https://www.dagstuhl.de/dagpub/978-3-95977-389-8

Turon, A. J., Thamsborg, J., Ahmed, A., Birkedal, L. & Dreyer, D. (2013). Logical relations for fine-grained concurrency. In POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 343-356). Association for Computing Machinery. https://doi.org/10.1145/2429069.2429111

Turon, A., Dreyer , D. & Birkedal, L. (2013). Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In G. Morrisett & T. Uustalu (Eds.), Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13 (pp. 377-390 ). Association for Computing Machinery. https://doi.org/10.1145/2500365.2500600

Tunç, H. C., Mathur, U., Pavlogiannis, A. & Viswanathan, M. (2023). Sound Dynamic Deadlock Prediction in Linear Time. Proceedings of the ACM on Programming Languages , 7, 1733-1758. https://doi.org/10.1145/3591291

Tunç, H. C., Abdulla, P. A., Chakraborty, S., Krishna, S., Mathur, U. & Pavlogiannis, A. (2023). Optimal Reads-From Consistency Checking for C11-Style Memory Models. Proceedings of the ACM on Programming Languages , 7(PLDI), 761–785. Article 137. https://doi.org/10.1145/3591251

Tunç, H. C., Deshmukh, A. P., Çirisci, B., Enea, C. & Pavlogiannis, A. (2024). CSSTs: A Dynamic Data Structure for Partial Orders in Concurrent Execution Analysis. In ASPLOS '24: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (Vol. 3, pp. 223-238). Association for Computing Machinery. https://doi.org/10.1145/3620666.3651358

Tunç, H. C., Dong, Y., Deshmukh, A. P., Cirisci, B., Enea, C. & Pavlogiannis, A. (2025). Efficient Dynamic Concurrency Analysis with Collective Sparse Segment Trees. ACM transactions on computer systems. Advance online publication. https://doi.org/10.1145/3773085

Torp-Smith, N., Birkedal, L. & Reynolds, J. C. (2008). Local Reasoning about a Copying Garbage Collector. A C M Transactions on Programming Languages and Systems, 30(4), 24-81.

Tofte, M. & Birkedal, L. (1998). A Region Inference Algorithm. A C M Transactions on Programming Languages and Systems, 20(4), 724-767. http://www.scopus.com/inward/record.url?scp=0032108162&partnerID=8YFLogxK

Tofte, M., Birkedal, L., Elsman, M. & Hallenberg, N. (2004). A retrospective on Region-based Memory Management. Higher-Order and Symbolic Computation, 17(3), 245-265. https://doi.org/10.1023/B:LISP.0000029446.78563.a4

Tofte, M. & Birkedal, L. (2000). Unification and polymorphism in region inference: essays in honour of Robin Milner. In G. Plotkin , C. Stirling & M. Tofte (Eds.), Proof, language, and interaction (pp. 389-423 ). MIT Press. http://dl.acm.org/citation.cfm?id=345868.345907&coll=DL&dl=GUIDE&CFID=560593603&CFTOKEN=90733199

Tkadlec, J., Pavlogiannis, A., Chatterjee, K. & Nowak, M. A. (2019). Population structure determines the tradeoff between fixation probability and fixation time. Communications Biology, 2(1), Article 138. https://doi.org/10.1038/s42003-019-0373-y

Tkadlec, J., Pavlogiannis, A., Chatterjee, K. & Nowak, M. A. (2020). Limits on amplifiers of natural selection under death-Birth updating. PLoS Computational Biology, 16(1), Article e1007494. https://doi.org/10.1371/journal.pcbi.1007494

Tkadlec, J., Pavlogiannis, A., Chatterjee, K. & Nowak, M. A. (2021). Fast and strong amplifiers of natural selection. Nature Communications, 12(1), Article 4009. https://doi.org/10.1038/s41467-021-24271-w

Timany, A., Stefanesco, L., Krogh-Jespersen, M. & Birkedal, L. (2018). A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST. In Proceedings of the ACM on Programming Languages (Vol. 2, pp. 64:00-64:28). Association for Computing Machinery. https://doi.org/10.1145/3158152

Timany, A. & Birkedal, L. (2019). Mechanized relational verification of concurrent programs with continuations. Proceedings of the ACM on Programming Languages , 3(ICFP), 1-28. Article 105. https://doi.org/10.1145/3341709

Timany, A. & Sozeau, M. (2018). Cumulative inductive types in coq. In H. Kirchner (Ed.), 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018 Article 29 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2018.29

Timany, A. & Birkedal, L. (2021). Reasoning about monotonicity in separation logic. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21) (pp. 91-104). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439931

Timany, A., Guéneau, A. & Birkedal, L. (2024). The Logical Essence of Well-Bracketed Control Flow. Proceedings of the ACM on Programming Languages , 8(POPL), 575-603. https://doi.org/10.1145/3632862

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, Article 9. https://doi.org/10.1145/3632851

Timany, A., Krebbers, R., Dreyer, D. & Birkedal, L. (2024). A Logical Approach to Type Soundness. Journal of the ACM, 71(6), Article 40. https://doi.org/10.1145/3676954

Thomsen, S. E. & Spitters, B. (2020). Formalizing Nakamoto-Style Proof of Stake.

Thomsen, S. E. & Spitters, B. (2021). Formalizing Nakamoto-Style Proof of Stake. In Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021 IEEE. https://doi.org/10.1109/CSF51468.2021.00042

Thamsborg, J. J. & Birkedal, L. (2011). A Kripke Logical Relation for Effect-Based Program Transformations. In ICFP 11. Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (pp. 445-456). Association for Computing Machinery. https://doi.org/10.1145/2034574.2034831

Thamsborg, J. J., Birkedal, L. & Yang, H. (2012). Two for the Price of One: Lifting Separation Logic Assertions. Logical Methods in Computer Science, 8(3).

Tan, J. & Madsen, M. (2025). Overloading the Dot. In D. Kluss, S. Achour & J. Palsberg (Eds.), CC 2025 - Proceedings of the 34th ACM SIGPLAN International Conference on Compiler Construction (pp. 60-69). Association for Computing Machinery. https://doi.org/10.1145/3708493.3712684

Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K. & Nowak, M. A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports, 12, Article 1526. https://doi.org/10.1038/s41598-022-05333-5

Svendsen, K. & Birkedal, L. (2014). Impredicative concurrent abstract predicates. In Z. Shao (Ed.), Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (pp. 149-168 ). Springer. https://doi.org/10.1007/978-3-642-54833-8_9

Svendsen, K., Birkedal, L. & Nanevski, A. (2011). Partiality, State, and Dependent Types. In Proceedings of Typed LAmbda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011 (Vol. LNCS 6690, pp. 198-212). Springer.

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Higher-order Concurrent Abstract Predicates.

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Verification of the Joins Library in Higher-Order Separation Logic. http://www.itu.dk/people/kasv/joins-tr.pdf

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Modular Reasoning about Separation of Concurrent Data Structures. In M. Felleisen & P. Gardner (Eds.), Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (pp. 169-188 ). Springer. https://doi.org/10.1007/978-3-642-37036-6_11

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Joins: A case study in modular specification of a concurrent reentrant higher-order library. In G. Castagna (Ed.), 27th European Conference on Object-Oriented Programming, ECOOP 2013; Montpellier; France (pp. 327-351). Springer. https://doi.org/10.1007/978-3-642-39038-8_14

Svendsen, K., Birkedal, L. & Parkinson, M. (2010). Verifying generics and delegates. In ECOOP 2010 – Object-Oriented Programming: 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings (pp. 175-199). Springer. https://doi.org/10.1007/978-3-642-14107-2_9

Svendsen, K., Buisse, A. & Birkedal, L. (2008). Verifying design patterns in Hoare type theory. IT University of Copenhagen. I T University. Technical Report Series No. TR-2008-112

Svendsen, K., Sieczkowski, F. & Birkedal, L. (2016). Transfinite step-indexing: Decoupling concrete and logical steps. In P. Thiemann (Ed.), Programming Languages and Systems (Vol. 9632, pp. 727-751). Springer VS. https://doi.org/10.1007/978-3-662-49498-1_28

Strydonck, T. V., Georges, A. L., Guéneau, A., Trieu, A., Timany, A., Piessens, F., Birkedal, L. & Devriese, D. (2022). Proving full-system security properties under multiple attacker models on capability machines. In Proceedings - 2022 IEEE 35th Computer Security Foundations Symposium, CSF 2022 (pp. 80-95). IEEE. https://doi.org/10.1109/CSF54842.2022.9919645

Stiévenart, Q. & Madsen, M. (2020). Fuzzing channel-based concurrency runtimes using types and effects. In Proceedings of the ACM on Programming Languages (OOPSLA ed., Vol. 4). Association for Computing Machinery. https://doi.org/10.1145/3428254

Sterling, J., Angiuli, C. & Gratzer, D. (2019). Cubical syntax for reflection-free extensional equality. In H. Geuvers (Ed.), 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019 Article 31 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2019.31

Displaying results 1 to 50 out of 533

Revised 05.12.2025

Marianne Dammand Iversen