Publications

Sort by: Date | Author | Title

Conrado, G. K. & Pavlogiannis, A. (2024). A Better Approximation for Interleaved Dyck Reachability. In SOAP 2024 - Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (pp. 18-25). Association for Computing Machinery. https://doi.org/10.1145/3652588.3663318

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. Article 243. https://doi.org/10.1145/3674632

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

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. Article 21. https://doi.org/10.1145/3632863

Lutze, M. & Madsen, M. (2024). Associated Effects: Flexible Abstractions for Effectful Programming. Proceedings of the ACM on Programming Languages , 8, Article 163. https://doi.org/10.1145/3656393

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), Article 26. https://doi.org/10.1145/3632868

Schenck, R., Hinnerskov, N. H., Henriksen, T., Madsen, M. & Elsman, M. (2024). AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming. Proceedings of the ACM on Programming Languages , 8(OOPSLA2), 1787-1813. Article 334. https://doi.org/10.1145/3689774

Saioc, G.-V., Lange, J. & Møller, A. (2024). Automated Verification of Parametric Channel-Based Process Communication. In Proceedings of the ACM on Programming Languages (Vol. 8, pp. 2070-2096). Article 344 https://doi.org/10.1145/3689784

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), Article 3. https://doi.org/10.1145/3623510

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

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

Jakobsen, A. B., Jørgensen, R. S. M., van de Pol, J. & Pavlogiannis, A. (2024). Fast Symbolic Computation of Bottom SCCs. In B. Finkbeiner & L. Kovács (Eds.), Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024 (pp. 110-128). Springer. https://doi.org/10.1007/978-3-031-57256-2_6

Chakraborty, S., Krishna, S. N., Mathur, U. & Pavlogiannis, A. (2024). How Hard Is Weak-Memory Testing? Proceedings of the ACM on Programming Languages , 8, Article 66. https://doi.org/10.1145/3632908

Shaik, I., Mayer-Eichberger, V., van de Pol, J. & Saffidine, A. (2024). Implicit QBF Encodings for Positional Games. In M. Hartisch, C.-H. Hsueh & J. Schaeffer (Eds.), Advances in Computer Games - 18th International Conference, ACG 2023, Revised Selected Papers (pp. 133-145). Springer. https://doi.org/10.1007/978-3-031-54968-7_12

Chakraborty, M., Gnanakumar, A., Sridharan, M. & Møller, A. (2024). Indirection-Bounded Call Graph Analysis. In J. Aldrich & G. Salvaneschi (Eds.), 38th European Conference on Object-Oriented Programming, ECOOP 2024 Article 3 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2024.10

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), Article 282. https://doi.org/10.1145/3689722

Nelson, B., Pagnin, E. & Askarov, A. (2024). Metadata Privacy Beyond Tunneling for Instant Messaging. In Proceedings - 9th IEEE European Symposium on Security and Privacy, EuroS&P 2024 (pp. 697-723). IEEE. https://doi.org/10.1109/EuroSP60621.2024.00044

Protzenko, J. & Spitters, B. (2024). Modernizing FIPS for safe languages and verified libraries. Paper presented at NIST Workshop on Formal Methods within Certification Programs (FMCP 2024), Rockville, Maryland, United States. https://www.nist.gov/system/files/documents/2024/06/11/08-ProtzenkoSpitters.pdf

Frumin, D., Timany, A. & Birkedal, L. (2024). Modular Denotational Semantics for Effects with Guarded Interaction Trees. Proceedings of the ACM on Programming Languages , 8(POPL), Article 12. https://doi.org/10.1145/3632854

Sølvsten, S. & van de Pol, J. (2024). Multi-variable Quantification of BDDs in External Memory using Nested Sweeping. ArXiv. https://doi.org/10.48550/arXiv.2408.14216

Dahlsen-Jensen, M. B., Fievet, B., Petrucci, L. & de Pol, J. V. (2024). On-The-Fly Algorithm for Reachability in Parametric Timed Games. In B. Finkbeiner & L. Kovács (Eds.), 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 (pp. 194-212). Springer Science+Business Media. https://doi.org/10.1007/978-3-031-57256-2_10

Krishna, S., Lal, A., Pavlogiannis, A. & Tuppe, O. (2024). On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability. Proceedings of the ACM on Programming Languages , 8(POPL), 1239-1268. https://doi.org/10.1145/3632884

Neele, T. & Pol, J. V. D. (2024). Operations on Fixpoint Equation Systems. Logical Methods in Computer Science, 20(3), 5:1-5:32. https://doi.org/10.46298/LMCS-20(3:5)2024

Shaik, I. & Pol, J. V. D. (2024). Optimal Layout-Aware CNOT Circuit Synthesis with Qubit Permutation. In U. Endriss, F. S. Melo, K. Bach, A. Bugarin-Diz, J. M. Alonso-Moral, S. Barro & F. Heintz (Eds.), ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain - Including 13th Conference on Prestigious Applications of Intelligent Systems (PAIS 2024) (pp. 4207-4215). IOS Press. https://doi.org/10.3233/FAIA240993

Shaik, I. & Van de Pol, J. (2024). Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits. In S. Chakraborty & J.-H. R. Jiang (Eds.), 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024 Article 26 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SAT.2024.26

Shi, Z., Mathur, U. & Pavlogiannis, A. (2024). Optimistic Prediction of Synchronization-Reversal Data Races. In ICSE 2024 - Proceedings of the 46th IEEE/ACM International Conference on Software Engineering: Proceedings of the IEEE/ACM 46th International Conference on Software Engineering (pp. 1-13). Article 134 Association for Computing Machinery. https://doi.org/10.1145/3597503.3639099

Ma, W., Egger, M. K., Pavlogiannis, A., Li, Y. & Karras, P. (2024). Reachability-Aware Fair Influence Maximization. In W. Zhang, Z. Yang, X. Wang, A. Tung, Z. Zheng & H. Guo (Eds.), Web and Big Data - 8th International Joint Conference, APWeb-WAIM 2024, Proceedings: 8th International Joint Conference, APWeb-WAIM 2024, Jinhua, China, August 30 – September 1, 2024, Proceedings, Part III (pp. 342-359). BMJ, Springer Nature. https://doi.org/10.1007/978-981-97-7238-4_22

Laursen, M. R., Xu, W. & Møller, A. (2024). Reducing Static Analysis Unsoundness with Approximate Interpretation. Proceedings of the ACM on Programming Languages , 8, 1165-1188. https://doi.org/10.1145/3656424

Petsinis, P., Zhang, K., Pavlogiannis, A., Zhou, J. & Karras, P. (2024). Robust Reward Placement under Uncertainty. In K. Larson (Ed.), Proceedings of the 33rd International Joint Conference on Artificial Intelligence, IJCAI 2024 (pp. 6770-6778). International Joint Conferences on Artificial Intelligence Organization. https://doi.org/10.24963/ijcai.2024/748

Berger, C. P., Lutze, M. C. D., Elmqvist, N., Madsen, M. & Klokmose, C. N. (2024). Scientists and Code: Programming as a Tool. Paper presented at PLATEAU, Berkeley, California, United States. https://kilthub.cmu.edu/articles/conference_contribution/Scientists_and_Code_Programming_as_a_Tool/25587726?backTo=/collections/PLATEAU_2024/7093870

Petsinis, P., Pavlogiannis, A., Tkadlec, J. & Karras, P. (2024). Seed Selection in the Heterogeneous Moran Process. In K. Larson (Ed.), Proceedings of the 33rd International Joint Conference on Artificial Intelligence, IJCAI 2024 (pp. 2297-2305). International Joint Conferences on Artificial Intelligence Organization. https://doi.org/10.24963/ijcai.2024/254

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. Article 313. https://doi.org/10.1145/3689753

Sieczkowski, F., Stepanenko, S., Sterling, J. & Birkedal, L. (2024). The Essence of Generalized Algebraic Data Types. Proceedings of the ACM on Programming Languages , 8(POPL), 695-723. https://doi.org/10.1145/3632866

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

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

Sterling, J., Gratzer, D. & Birkedal, L. (2024). Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. In A. Murano & A. Silva (Eds.), 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024 Article 47 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2024.47

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

Pientka, B., Blazy, S., Traytel, D. & Timany, A. (2024). Welcome from the Chairs. In CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024 (pp. iii-iv)

Aagaard, F. L., Sterling, J. & Birkedal, L. (2023). A denotationally-based program logic for higher-order store. Electronic Notes in Theorical Informatics and Computer Science, 3. https://doi.org/10.46298/entics.12232

Sølvsten, S. & van de Pol, J. (2023). Adiar 1.1: Zero-Suppressed Decision Diagrams in External Memory. In K. Y. Rozier & S. Chaudhuri (Eds.), NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings (pp. 464-471). Springer. https://doi.org/10.1007/978-3-031-33170-1_28

Gleirscher, M., van de Pol, J. & Woodcock, J. (2023). A manifesto for applicable formal methods. Software and Systems Modeling, 22(6), 1737-1749. https://doi.org/10.1007/s10270-023-01124-2

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

Starup, J. L., Madsen, M. & Lhoták, O. (2023). Breaking the Negative Cycle: Exploring the Design Space of Stratification for First-Class Datalog Constraints. In K. Ali & G. Salvaneschi (Eds.), 37th European Conference on Object-Oriented Programming, ECOOP 2023 Article 31 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2023.31

Shaik, I. & van de Pol, J. (2023). Concise QBF Encodings for Games on a Grid (extended version). https://doi.org/10.48550/arXiv.2303.16949

Madsen, M., Van De Pol, J. & Henriksen, T. (2023). Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems. Proceedings of the ACM on Programming Languages , 7(OOPSLA2), 516–543. Article 240. https://doi.org/10.1145/3622816

Aranha, D. F., Hvass, B. S., Spitters, B. & Tibouchi, M. (2023). Faster constant-time evaluation of the Kronecker symbol with application to elliptic curve hashing. In CCS'23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 3228-3238). Association for Computing Machinery. https://doi.org/10.1145/3576915.3616597

Nielsen, E. H., Annenkov, D. & Spitters, B. (2023). Formalising Decentralised Exchanges in Coq. In R. Krebbers, D. Traytel, B. Pientka & S. Zdancewic (Eds.), CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 290-302). Association for Computing Machinery. https://doi.org/10.1145/3573105.3575685

Hvass, B. S., Aranha, D. F. & Spitters, B. (2023). High-assurance field inversion for curve-based cryptography. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF) (pp. 552-567). IEEE. https://doi.org/10.1109/CSF57540.2023.00008

Shaik, I., Mayer-Eichberger, V., van de Pol, J. & Saffidine, A. (2023). Implicit State and Goals in QBF Encodings for Positional Games (extended version). https://doi.org/10.48550/arXiv.2301.07345

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

Displaying results 51 to 100 out of 544

Revised 05.12.2025

Marianne Dammand Iversen