Publications

Sort by: Date | Author | Title

Madsen, M. & Møller, A. (2014). Sparse Dataflow Analysis with Pointers and Reachability. In M. Müller-Olm & H. Seidl (Eds.), Static Analysis: 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings (pp. 201-218). Springer VS. https://doi.org/10.1007/978-3-319-10936-7_13

Madsen, M., Tip, F., Andreasen, E. S., Sen, K. & Møller, A. (2016). Feedback-directed instrumentation for deployed JavaScript applications. In Proceedings - 2016 IEEE/ACM 38th IEEE International Conference on Software Engineering Companion, ICSE 2016: ICSE 2016 (pp. 899-910). Association for Computing Machinery. https://doi.org/10.1145/2884781.2884846

Madsen, M., Zarifi, R. & Lhoták, O. (2018). Tail Call Elimination and Data Representation for Functional Languages on the Java Virtual Machine. In J. Xue & C. Dubach (Eds.), CC 2018 - Proceedings of the 27th International Conference on Compiler Construction, Co-located with CGO 2018 (pp. 139-150). Association for Computing Machinery. https://doi.org/10.1145/3178372.3179499

Madsen, M. & Lhoták, O. (2018). Safe and Sound Program Analysis with Flix. In E. Bodden & F. Tip (Eds.), ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 38-48). Association for Computing Machinery. https://doi.org/10.1145/3213846.3213847

Madsen, M. & Lhoták, O. (2018). Implicit Parameters for Logic Programming. In D. Sabel & P. Thiemann (Eds.), Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming Article 14 Association for Computing Machinery. https://doi.org/10.1145/3236950.3236953

Madsen, M., Livshits, B. & Fanning, M. (2013). Practical static analysis of JavaScript applications in the presence of frameworks and libraries. In B. Meyer, L. Baresi & M. Mezini (Eds.), Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering , ESEC/FSE 2013 (pp. 499-509). Association for Computing Machinery. https://doi.org/10.1145/2491411.2491417

Madsen, M., Lhoták, O. & Tip, F. (2020). A Semantics for the Essence of React. In R. Hirschfeld & T. Pape (Eds.), 34th European Conference on Object-Oriented Programming (ECOOP 2020) (Vol. 166, pp. 12:1-12:26). Article 12 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2020.12

Madsen, M. & Lhoták, O. (2020). Fixpoints for the masses: programming with first-class Datalog constraints. In Proceedings of the ACM on Programming Languages (OOPSLA ed., Vol. 4). Association for Computing Machinery. https://doi.org/10.1145/3428193

Madsen, M. & Pol, J. V. D. (2020). Polymorphic types and effects with Boolean unification. In Proceedings of the ACM on Programming Languages (OOPSLA ed., Vol. 4). Association for Computing Machinery. https://doi.org/10.1145/3428222

Madsen, M. & Van De Pol, J. (2021). Relational nullable types with Boolean unification. Proceedings of the ACM on Programming Languages , 5(OOPSLA), 1-28. Article 110. https://doi.org/10.1145/3485487

Madsen, M. (2022). The Principles of the Flix Programming Language. In Onward! 2022 - Proceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, co-located with SPLASH 2022 (pp. 112-127). Association for Computing Machinery. https://doi.org/10.1145/3563835.3567661

Madsen, M., Starup, J. L. & Lhoták, O. (2022). Flix: A Meta Programming Language for Datalog. In Proceedings of the 4th International Workshop on the Resurgence of Datalog in Academia and Industry (Datalog-2.0 2022) (pp. 202-206). CEUR-WS.org. https://ceur-ws.org/Vol-3203/short8.pdf

Madsen, M., Starup, J. L. & Lutze, M. (2023). Restrictable Variants: A Simple and Practical Alternative to Extensible Variants. In K. Ali & G. Salvaneschi (Eds.), 37th European Conference on Object-Oriented Programming, ECOOP 2023 (pp. 17:1-17:27). Article 17 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2023.17

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

Madsen, M. & Pol, J. V. D. (2023). Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism. In K. Ali & G. Salvaneschi (Eds.), 37th European Conference on Object-Oriented Programming (ECOOP 2023) Article 18 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2023.18

Madsen, M. (2015). Static Analysis of Dynamic Languages. Department of Computer Science, Aarhus University.

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

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

Lutze, M., Madsen, M., Schuster, P. & Brachthäuser, J. I. (2023). With or Without You: Programming with Effect Exclusion. Proceedings of the ACM on Programming Languages , 7(ICFP), 448-475. https://doi.org/10.1145/3607846

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

Livshits, B., Sridharan, M., Smaragdakis, Y., Lhoták, O., Amaral, J. N., Chang, B.-Y. E., Guyer, S. Z., Khedker, U. P., Møller, A. & Vardoulakis, D. (2015). In Defense of Soundiness: A Manifesto. Communications of the A C M, 58(2). https://doi.org/10.1145/2644805

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

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. Advance online publication. https://doi.org/10.1145/3786762

Licata, D. R., Orton, I., Pitts, A. M. & Spitters, B. (2018, Jul 1). Internal Universes in Models of Homotopy Type Theory. arxiv.org. https://doi.org/10.4230/LIPIcs.FSCD.2018.22

Li, Y., Tan, T., Møller, A. & Smaragdakis, Y. (2018). Precision-Guided Context Sensitivity for Pointer Analysis. Proceedings of the ACM on Programming Languages , 2(OOPSLA), 141:1-141:29. Article 141. https://doi.org/10.1145/3276511

Li, Y., Tan, T., Møller, A. & Smaragdakis, Y. (2018). Scalability-First Pointer Analysis with Self-Tuning Context-Sensitivity. In G. T. Leavens, A. Garcia & C. S. Păsăreanu (Eds.), ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering (pp. 129-140). Association for Computing Machinery. https://doi.org/10.1145/3236024.3236041

Li, Y., Tan, T., Møller, A. & Smaragdakis, Y. (2020). A Principled Approach to Selective Context Sensitivity for Pointer Analysis. ACM Transactions on Programming Languages and Systems, 42(2), Article 10. https://doi.org/10.1145/3381915

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

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

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

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

Kulkarni, R., Mathur, U. & Pavlogiannis, A. (2021). Dynamic Data-Race Detection Through the Fine-Grained Lens. In S. Haddad & D. Varacca (Eds.), 32nd International Conference on Concurrency Theory (CONCUR 2021) (pp. 16:1-16:23). Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2021.16

Krogh-Jespersen, M., Svendsen, K. & Birkedal, L. (2017). A relational model of types-and-effects in higher-order concurrent separation logic. In POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages: POPL 2017 (pp. 218-231). Association for Computing Machinery. https://doi.org/10.1145/3009837.3009877

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

Kristensen, E. K. & Møller, A. (2017). Type Test Scripts for TypeScript Testing. Proceedings of the ACM on Programming Languages , 1(OOPSLA), 90:1-90:25. Article 90. https://doi.org/10.1145/3133914

Kristensen, E. K. & Møller, A. (2017). Inference and Evolution of TypeScript Declaration Files. In M. Huisman & J. Rubin (Eds.), Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings: 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Vol. 10202, pp. 99-115). Springer VS. https://doi.org/10.1007/978-3-662-54494-5_6

Kristensen, E. K. & Møller, A. (2019). Reasonably-Most-General Clients for JavaScript Library Analysis. Proceedings of the International Conference on Software Engineering, 83-93. https://doi.org/10.1109/ICSE.2019.00026

Krishnaswami, N., Birkedal, L. & Aldrich, J. (2010). Verifying event-driven programs using ramified frame properties. In A. Kennedy & N. Benton (Eds.), {Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010 (pp. 63-76). Association for Computing Machinery. https://doi.org/10.1145/1708016.1708025

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

Krishnaswam, N. R. K., Aldrich, J. & Birkedal, L. (2007). Modular Verification of the Subject-Observer Pattern via Higher-order Separation Logic. In Proceedings of 9th Workshop on Formal Techniques for Java-like Programs, FTfJP Fakultät für Informatik, Universität Magdeburg. http://www.cs.cmu.edu/~neelk/observer.pdf

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

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. & Spitters, B. (2013). Type classes for efficient exact real arithmetic in CoQ. Logical Methods in Computer Science, 9(1). https://doi.org/10.2168/LMCS-9(1:01)2013

Krebbers, R. & Spitters, B. (2011). Computer certified efficient exact reals in Coq. In Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Proceedings (pp. 90-106) https://doi.org/10.1007/978-3-642-22673-1_7

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

Kordon, F., Leuschel, M., Pol, J. V. D. & Thierry-Mieg, Y. (2019). Software Architecture of Modern Model Checkers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): State of the Art and Perspectives (pp. 393-419). Springer. https://doi.org/10.1007/978-3-319-91908-9_20

Klarlund, N. & Møller, A. (2001). MONA Version 1.4 User Manual. BRICS Notes Series, (NS-01-1).

Klarlund, N., Møller, A. & Schwartzbach, M. I. (2002). MONA Implementation Secrets. International Journal of Foundations of Computer Science, 13(4), 571-586. https://doi.org/10.1142/S012905410200128X

Klarlund, N., Møller, A. & Schwartzbach, M. I. (2002). The DSD Schema Language. Automated Software Engineering, 9(3), 285-319. https://doi.org/10.1023/A:1016376608070

Displaying results 201 to 250 out of 533

Revised 05.12.2025

Marianne Dammand Iversen