Find

For students
For PhDs
For employees

Department of Computer Science

Publications

Sort by: Date | Author | Title

Dahlsen-Jensen, M. B. & van de Pol, J. (2027). Random Generation of Small Quantitative Automata for Algorithm Debugging. In G. De Giacomo, J. Li & L. Xiao (Eds.), Theoretical Aspects of Software Engineering: 20th International Symposium, TASE 2026, Shanghai, China, July 4–6, 2026, Proceedings (pp. 188-205). Springer. https://doi.org/10.1007/978-3-032-30693-7_13

Sosso, A., Arora, A. & Spitters, B. (2026). Agentic Proving for Program Verification. Abstract from ICLR 2026 Workshop on Logical Reasoning of Large Language Models, Rio de Janeiro, Brazil. https://openreview.net/forum?id=wpQ6rTpGY6

Sosso, A., Arora, A. & Spitters, B. (2026). Agentic Proving for Program Verification.

Sosso, A. & Spitters, B. (2026). Agentic Proving for Type Theory. Abstract from 32nd International Conference on Types for Proofs and Programs, Gothenburg, Sweden. https://types2026.cse.chalmers.se/abstracts/64.pdf

Liu, Z., Hammond, A., Pérami, T., Sewell, P., Birkedal, L. & Pichon-Pharabod, J. (2026). An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics. ACM Transactions on Programming Languages and Systems, 48(1), Article 3. https://doi.org/10.1145/3786762

Goharshady, A. K., Lam, C. K., Pavlogiannis, A. & Zaher, A. K. (2026). A New Approach to Optimal Function Inlining for Code Size Minimization via E-graphs. Proceedings of the ACM on Programming Languages , 10(OOPSLA2), Article 367. https://doi.org/10.1145/3839499

Conrado, G. K. & Pavlogiannis, A. (2026). An MSO Framework for Weak-Memory Verification and Robustness. In A. Sokolova & P. Totzke (Eds.), 37th International Conference on Concurrency Theory, CONCUR 2026 Article 25 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2026.25

Rousseau, J., Carnier, D., Van Strydonck, T., Keuchel, S., Devriese, D. & Birkedal, L. (2026). Cerisier: A Program Logic for Attestation in a Capability Machine. Proceedings of the ACM on Programming Languages , 10, Article 209. https://doi.org/10.1145/3808287

Li, K. H., Aguirre, A., Tassarotti, J. & Birkedal, L. (2026). Contextual Refinement of Higher-Order Concurrent Probabilistic Programs. Proceedings of the ACM on Programming Languages , 10, Article 187. https://doi.org/10.1145/3808265

Tunç, H. C., Dong, Y., Deshmukh, A. P., Cirisci, B., Enea, C. & Pavlogiannis, A. (2026). Efficient Dynamic Concurrency Analysis with Collective Sparse Segment Trees. ACM Transactions on Computer Systems, 44(3). https://doi.org/10.1145/3773085

Kjelstrøm, A. H., Pavlogiannis, A. & van de Pol, J. (2026). Efficient Simulation of High-Level Quantum Gates. Quantum, 10. https://doi.org/10.22331/q-2026-05-05-2093

Tunç, H. C., Dong, Y. & Pavlogiannis, A. (2026). Fast Atomicity Monitoring. Proceedings of the ACM on Programming Languages , 10, Article 170. https://doi.org/10.1145/3808248

Madsen, M., Larsen, A. S., Villumsen, J. S. & Askarov, A. (2026). Fighting Supply Chain Attacks with Effect Systems. Proceedings of the ACM on Programming Languages , 10(OOPSLA2), Article 362. https://doi.org/10.1145/3839494

Legoupil, M., Pedersen, M., Birkedal, L., Lindley, S. & Pichon-Pharabod, J. (2026). Iris-WasmFX: Modular Reasoning for Wasm Stack Switching. Proceedings of the ACM on Programming Languages , 10, Article 193. https://doi.org/10.1145/3808271

Xu, W. & Møller, A. (2026). JavaScript Pointer Analysis with Adaptive Heap Abstraction. Proceedings of the ACM on Software Engineering, 3(FSE), 832 - 852. Article FSE038. https://doi.org/10.1145/3797133

Namakonov, E., Fasse, J., Jacobs, B., Birkedal, L. & Timany, A. (2026). Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic. Proceedings of the ACM on Programming Languages , 10(OOPSLA1), Article 132. https://doi.org/10.1145/3798240

Marionneau, V., Sassus Bourda, F., Aguirre, A. & Birkedal, L. (2026). Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic. In K. Stark, Y. Zakowski, N. Swamy & N. Tabareau (Eds.), CPP 2026 - Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2026 (pp. 368-382) https://doi.org/10.1145/3779031.3779109

Haselwarter, P. G., Aguirre, A., Gregersen, S. O., Li, K. H., Tassarotti, J. & Birkedal, L. (2026). Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic. Proceedings of the ACM on Programming Languages , 10, Article 233. https://doi.org/10.1145/3808311

Milkevych, K. V., Van De Pol, J. & Shaik, I. (2026). Practical Subarchitectures for Optimal Quantum Layout Synthesis. In Proceedings - 2026 IEEE/ACM International Workshop on Quantum Software Engineering, Q-SE 2026 (pp. 33-41). Association for Computing Machinery. https://doi.org/10.1145/3786150.3788609

Gratzer, D., Shulman, M. & Sterling, J. (2026). STRICT UNIVERSES FOR GROTHENDIECK TOPOI. Theory and Applications of Categories, 45, 1227-1279.

Gratzer, D., Weinberger, J. & Buchholtz, U. (2026). The ∞-Category of ∞-Categories in Simplicial Type Theory. In F. Claudia, K. Joost-Pieter & K. Joost-Pieter (Eds.), 41st Annual Symposium on Logic in Computer Science, LICS 2026 Article 52 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.LICS.2026.52

Shi, Z., Møldrup, L., Mathur, U. & Pavlogiannis, A. (2026). The Complexity of Testing Message-Passing Concurrency. Proceedings of the ACM on Programming Languages , 10, 1-32. https://doi.org/10.1145/3776643

Hansen, R. R., Larsen, A. S. & Askarov, A. (2026). The Downgrading Semantics of Memory Safety. Proceedings of the ACM on Programming Languages , 10, 328-355. https://doi.org/10.1145/3808260

Namakonov, E. S., Birkedal, L. & Timany, A. (2026). Verifying Wait-Freedom for Concurrent Higher-Order Programs. In R. Krebbers & A. Silva (Eds.), 40th European Conference on Object-Oriented Programming, ECOOP 2026 Article 20 https://doi.org/10.4230/LIPIcs.ECOOP.2026.20

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

Gratzer, D. (2025). A Modal Deconstruction of Löb Induction. Proceedings of the ACM on Programming Languages , 9, Article 30. https://doi.org/10.1145/3704866

Haselwarter, P. G., Li, K. H., Aguirre, A., Gregersen, S. O., Tassarotti, J. & Birkedal, L. (2025). Approximate Relational Reasoning for Higher-Order Probabilistic Programs. Proceedings of the ACM on Programming Languages , 9(POPL), 1196-1226. Article 41. https://doi.org/10.1145/3704877

Møldrup, L. & Pavlogiannis, A. (2025). AWDIT: An Optimal Weak Database Isolation Tester. Proceedings of the ACM on Programming Languages , 9, 1540-1564. Article 209. https://doi.org/10.1145/3742465

Meier, W., Jensen, M., Pichon-Pharabod, J. & Spitters, B. (2025). CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq. In Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 127-139). Association for Computing Machinery. https://doi.org/10.1145/3703595.3705879

Conrado, G. K. & Pavlogiannis, A. (2025). CFL-based methods for approximating interleaved Dyck reachability. International Journal on Software Tools for Technology Transfer, 27(2), 255-266. Article 106135. https://doi.org/10.1007/s10009-025-00787-0

Shaik, I. & van de Pol, J. (2025). CNOT-Optimal Clifford Synthesis as SAT. In J. Berg, J. Nordstrom & J. Nordstrom (Eds.), 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025 Article 28 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SAT.2025.28

Stepanenko, S., Nardino, E., Frumin, D., Timany, A. & Birkedal, L. (2025). Context-Dependent Effects in Guarded Interaction Trees. In V. Vafeiadis (Ed.), Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings (Vol. Part II, pp. 286-313). Springer. https://doi.org/10.1007/978-3-031-91121-7_12

Dahlsen-Jensen, M. B., Fievet, B., Petrucci, L. & van de Pol, J. (2025). Controller Synthesis for Parametric Timed Games. In P. Prabhakar & A. Vandin (Eds.), Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, QEST+FORMATS 2025, Proceedings (pp. 314-332). Springer Science+Business Media. https://doi.org/10.1007/978-3-032-05792-1_17

Gratzer, D., Sterling, J., Angiuli, C., Coquand, T. & Birkedal, L. (2025). Controlling unfolding in type theory. Mathematical Structures in Computer Science, 35, Article e38. https://doi.org/10.1017/S0960129525100327

Jakobsen, A. B., Clausen, A. B., van de Pol, J. & Shaik, I. (2025). Depth-Optimal Quantum Layout Synthesis as SAT. In J. Berg & J. Nordstrom (Eds.), 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025 Article 16 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SAT.2025.16

Saioc, G.-V., Lee, I.-T. A., Møller, A. & Chabbi, M. (2025). Dynamic Partial Deadlock Detection and Recovery via Garbage Collection. In ASPLOS 2025 - Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (pp. 244-259). Association for Computing Machinery. https://doi.org/10.1145/3676641.3715990

Endo, A. T. & Møller, A. (2025). Event Race Detection for Node.js Using Delay Injections. In J. Aldrich & A. Silva (Eds.), 39th European Conference on Object-Oriented Programming, ECOOP 2025 Article 9 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2025.9

Madsen, M. & Lhoták, O. (2025). Flix: A Design for Language-Integrated Datalog. Proceedings of the ACM on Programming Languages , 9(OOPSLA2), 2115-2143. https://doi.org/10.1145/3763126

Bhargavan, K., Hansen, L. L., Kiefer, F., Schneider-Bensch, J. & Spitters, B. (2025). Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust. In CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security (pp. 2729-2743). Association for Computing Machinery. https://doi.org/10.1145/3719027.3765213

Chakraborty, S., Krishna, S., Pavlogiannis, A. & Tuppe, O. (2025). GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency. In R. Piskac & Z. Rakamaric (Eds.), Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings (pp. 321-346). Springer. https://doi.org/10.1007/978-3-031-98682-6_17

Bhargavan, K., Buyse, M., Franceschino, L., Hansen, L. L., Kiefer, F., Schneider-Bensch, J. & Spitters, B. (2025). hax: Verifying Security-Critical Rust Software Using Multiple Provers. In J. Protzenko & A. Raad (Eds.), Verified Software. Theories, Tools and Experiments - 16th International Conference, VSTTE 2024, Revised Selected Papers (pp. 96-119). Springer. https://doi.org/10.1007/978-3-031-86695-1_7

Gratzer, D., Møller, M. A. & Birkedal, L. (2025). Idempotent Resources in Separation Logic: The Heart of core in Iris. In P. A. Abdulla & D. Kesner (Eds.), Foundations of Software Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software: ETAPS 2025, Proceedings (pp. 45-66). Springer Science+Business Media. https://doi.org/10.1007/978-3-031-90897-2_3

Namakonov, E. S., Fasse, J., Jacobs, B., Birkedal, L. & Timany, A. (2025). Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic. Paper presented at Object-Oriented Programming, Systems, Languages & Applications 2026, Oakland, United States. Advance online publication.

Stassen, P., Møgelberg, R. E., Zwart, M. A., Aguirre, A. & Birkedal, L. (2025). Modelling Recursion and Probabilistic Choice in Guarded Type Theory. Proceedings of the ACM on Programming Languages , 9(POPL), 1417-1445. Article 48. https://doi.org/10.1145/3704884

Li, K. H., Aguirre, A., Gregersen, S. O., Haselwarter, P. G., Tassarotti, J. & Birkedal, L. (2025). Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. Proceedings of the ACM on Programming Languages , 9(ICFP), 276-305. https://doi.org/10.1145/3747514

Haselwarter, P. G., Aguirre, A., Gregersen, S. O., Tassarotti, J. & Birkedal, L. (2025). Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic.

Christensen, J. E., Jørgensen, S. F., Pavlogiannis, A. & van de Pol, J. (2025). On Exact Sizes of Minimal CNOT Circuits. In R. Glück & R. Kaarsgaard (Eds.), Reversible Computation: 17th International Conference, RC 2025, Proceedings (pp. 71-88). Springer. https://doi.org/10.1007/978-3-031-97063-4_6

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

Simner, B., Armstrong, A., Bauereiss, T., Campbell, B., Kammar, O., Pichon-Pharabod, J. & Sewell, P. (2025). Precise exceptions in relaxed architectures. In ISCA 2025 - Proceedings of the 52nd Annual International Symposium on Computer Architecture: Proceedings of the 52nd Annual International Symposium on Computer Architecture (pp. 211–224) https://doi.org/10.1145/3695053.3731102

Conrado, G. K., Kjelstrøm, A. H., Van De Pol, J. & Pavlogiannis, A. (2025). Program Analysis via Multiple Context Free Language Reachability. Proceedings of the ACM on Programming Languages , 9, Article 18. https://doi.org/10.1145/3704854

Displaying results 1 to 50 out of 554

1

Revised 05.12.2025

-

Marianne Dammand Iversen