Publications

Sort by: Date | Author | Title

Klarlund, N., Møller, A. & Schwartzbach, M. I. (2000). Document Structure Description 1.0. BRICS Notes Series, (NS-00-7).

Klarlund, N., Møller, A. & Schwartzbach, M. I. (2001). MONA Implementation Secrets. In S. Yu & A. Paun (Eds.), Implementation and Application of Automata: 5th International Conference, CIAA 2000 London, Ontario, Canada, July 24-25, 2000 Revised Papers (pp. 182-194). Springer. https://doi.org/10.1007/3-540-44674-5_4

Klarlund, N., Møller, A. & Schwartzbach, M. I. (2000). DSD: A Schema Language for XML. In Proceedings of the third workshop on Formal methods in software practice (pp. 101-111). Association for Computing Machinery. https://doi.org/10.1145/349360.351158

Kjelstrom, A. H. & Pavlogiannis, A. (2022). The Decidability and Complexity of Interleaved Bidirected Dyck Reachability. Proceedings of the ACM on Programming Languages , 6(POPL), Article 12. https://doi.org/10.1145/3498673

Kirkegaard, C., Møller, A. & Schwartzbach, M. I. (2004). Static Analysis of XML Transformations in Java. I E E E Transactions on Software Engineering, 30(3), 181-192. https://doi.org/10.1109/TSE.2004.1271173

Kirkegaard, C. & Møller, A. (2006). Static Analysis for Java Servlets and JSP. In K. Yi (Ed.), Static Analysis: 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006. Proceedings (pp. 336-352). Springer. https://doi.org/10.1007/11823230_22

Kirkegaard, C. & Møller, A. (2006). Type Checking with XML Schema in XACT. Paper presented at PLAN-X 2006: ACM SIGPLAN Workshop on Programming Language Technologies for XML, Charleston, SC, United States.

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

Kavvos, G. A. & Gratzer, D. (2023). Under Lock and Key: A Proof System for a Multimodal Logic. Bulletin of Symbolic Logic, 29(2), 264-293. https://doi.org/10.1017/bsl.2023.14

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., Krebbers, R., Birkedal, L. & Dreyer, D. (2016). Higher-order ghost state. In E. Sumii (Ed.), ICFP 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (pp. 256-269). Association for Computing Machinery. https://doi.org/10.1145/2951913.2951943

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, S. H., Møller, A. & Thiemann, P. (2009). Type Analysis for JavaScript. Lecture Notes in Computer Science, 5673, 238–255. https://doi.org/10.1007/978-3-642-03237-0_17

Jensen, S. H., Møller, A. & Thiemann, P. (2010). Interprocedural Analysis with Lazy Propagation. Lecture Notes in Computer Science, 6337, 320-339. https://doi.org/10.1007/978-3-642-15769-1_20

Jensen, S. H., Madsen, M. & Møller, A. (2011). Modeling the HTML DOM and Browser API in Static Analysis of JavaScript Web Applications. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering. ESEC/FSE '11 (pp. 59-69). Association for Computing Machinery. https://doi.org/10.1145/2025113.2025125

Jensen, S. H., Jonsson, P. A. & Møller, A. (2012). Remedying the Eval that Men Do. In M. Heimdahl & Z. Su (Eds.), 2012 International Symposium on Software Testing and Analysis (ISSTA) : Proceedings (pp. 34-44). Association for Computing Machinery. https://doi.org/10.1145/2338965.2336758

Jensen, C. S., Møller, A. & Su, Z. (2013). Server Interface Descriptions for Automated Testing of JavaScript Web Applications. In B. Meyer, L. Baresi & M. Mezini (Eds.), Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013 (pp. 510-520 ). Association for Computing Machinery. https://doi.org/10.1145/2491411.2491421

Jensen, C. S., Prasad, M. R. & Møller, A. (2013). Automated Testing with Targeted Event Sequence Generation. In M. Pezzè & M. Harman (Eds.), International Symposium on Software Testing and Analysis (ISSTA), 2013: Proceedings (pp. 67-77). Association for Computing Machinery. https://doi.org/10.1145/2483760.2483777

Jensen, J. B., Birkedal, L. & Sestoft, P. (2010). Modular verification of linked lists with views via separation logic. In Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs (pp. 4:1--4:7). Association for Computing Machinery. https://doi.org/10.1145/1924520.1924524

Jensen, J. B., Birkedal, L. & Sestoft, P. (2011). Modular Verification of Linked Lists with Views via Separation Logic. Journal of Object Technology, 10(1), 21-40. https://doi.org/10.5381/jot.2011.10.1.a2

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.

Jensen, J. B., Birkedal, L. & Sestoft, P. (2010). Modular verification of linked lists with views via separation logic. In FTFJP '10. Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs Article 4 Association for Computing Machinery. https://doi.org/10.1145/1924520.1924524

Jensen, C. S., Møller, A., Raychev, V., Dimitrov, D. & Vechev, M. (2015). Stateless Model Checking of Event-Driven Applications. In OOPSLA 2015 : Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (pp. 57-73). Association for Computing Machinery. https://doi.org/10.1145/2814270.2814282

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

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

Jacobs, K., Timany, A. & Devriese, D. (2021). Fully abstract from static to gradual. Proceedings of the ACM on Programming Languages , 5(POPL), Article 7. https://doi.org/10.1145/3434288

Jacobs, K., Devriese, D. & Timany, A. (2022). Purity of an ST monad: Full abstraction by semantically typed back-translation. Proceedings of the ACM on Programming Languages , 6(OOPSLA1), Article 82. https://doi.org/10.1145/3527326

Hvass, B. S., Aranha, D. F. & Spitters, B. (2020). High-assurance field inversion for pairing-friendly primes. Abstract from The Coq Workshop 2020. https://coq-workshop.gitlab.io/2020/abstracts/Coq2020_04-02-primes.pdf

Hvass, B. S., Aranha, D. F. & Spitters, B. (2020). High-assurance field inversion for pairing-friendly primes. Abstract from 2nd Workshop on Formal Methods for Blockchains. https://fmbc.gitlab.io/2020/files/FMBC2020.pdf

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

Huang, D., Morrisett, G. & Spitters, B. (2018, Jun 20). An Application of Computable Distributions to the Semantics of Probabilistic Programs. Cornell University.

Huang, D., Morrisett, G. & Spitters, B. (2020). Application of Computable Distributions to the Semantics of Probabilistic Programs. In G. Barthe, J.-P. Katoen & A. Silva (Eds.), Foundations of Probabilistic Programming (pp. 75-120). Cambridge University Press. https://doi.org/10.1017/9781108770750

Huang, D., Morrisett, G. & Spitters, B. (2020). Application ofComputable Distributions to the Semantics of Probabilistic Programs. In Foundations of Probabilistic Programming (pp. 75-120). Cambridge University Press. https://doi.org/10.1017/9781108770750.004

Heunen, C., Landsman, N. P. & Spitters, B. (2012). Bohrification of operator algebras and quantum logic. Synthese, 186(3), 719-752. https://doi.org/10.1007/s11229-011-9918-4

Heinze, T. S., Møller, A. & Strocco, F. (2016). Type safety analysis for dart. In R. Ierusalimschy (Ed.), DLS 2016 - Proceedings of the 12th Symposium on Dynamic Languages (pp. 1-12). Association for Computing Machinery. https://doi.org/10.1145/2989225.2989226

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

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

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

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

Hansen, J. C., Kjelstrøm, A. H. & Pavlogiannis, A. (2021). Tight bounds for reachability problems on one-counter and pushdown systems. Information Processing Letters, 171, Article 106135. https://doi.org/10.1016/j.ipl.2021.106135

Hansen, S. T., Gomes, C., Larsen, P. G. & Van De Pol, J. (2021). Synthesizing Co-Simulation Algorithms with Step Negotiation and Algebraic Loop Handling. In C. R. Martin, M. J. Blas & A. I. Psijas (Eds.), 2021 Annual Modeling and Simulation Conference (ANNSIM) (pp. 62-73). IEEE. https://doi.org/10.23919/ANNSIM52504.2021.9552073

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

Hansen, S. T., Thule, C., Gomes, C., van de Pol, J., Palmieri, M., Inci, E. O., Madsen, F., Alfonso, J., Castellanos, J. Á. & Rodriguez, J. M. (2022). Verification and synthesis of co-simulation algorithms subject to algebraic loops and adaptive steps. International Journal on Software Tools for Technology Transfer, 24(6), 999-1024. https://doi.org/10.1007/s10009-022-00686-8

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

Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B. & Strub, P.-Y. (2018, Jun 19). Computer-aided proofs for multiparty computation with active security. arxiv.org. https://arxiv.org/abs/1806.07197

Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B. & Strub, P. (2018). Computer-Aided Proofs for Multiparty Computation with Active Security. In Proceedings - IEEE 31st Computer Security Foundations Symposium, CSF 2018 (Vol. 2018, pp. 119-131). Article 8429300 IEEE. https://doi.org/10.1109/CSF.2018.00016

Guéneau, A., Hostert, J., Spies, S., Sammler, M., Birkedal, L. & Dreyer, D. (2023). Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proceedings of the ACM on Programming Languages , 7(OOPSLA2), 716-744. Article 247. https://doi.org/10.1145/3622823

Displaying results 251 to 300 out of 533

Revised 05.12.2025

Marianne Dammand Iversen