Publications

Sort by: Date | Author | Title

Schwinghammer, J., Birkedal, L., Reus, B. & Yang, H. (2011). Nested Hoare Triples and Frame Rules for Higher-Order Store. Logical Methods in Computer Science, 7(3:21), 440-454. https://doi.org/10.2168/LMCS-7(3:21)2011

Schwinghammer, J., Birkedal, L., Pottier, F., Reus, B., Støvring, K. & Yang, H. (2013). A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science, 23(1), 1-54. https://doi.org/10.1017/S0960129512000035

Schwinghammer, J. & Birkedal, L. (2011). Step-indexed relational reasoning for countable nondeterminism. In M. Bezem (Ed.), Computer Science Logic (CSL'11) : 25th International Workshop/20th Annual Conference of the EACSL (pp. 512-524). Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2011.512

Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F. & Reus, B. (2010). A semantic foundation for hidden state. In L. Ong (Ed.), Foundations of Software Science and Computational Structures: 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (pp. 2-17). Springer. https://doi.org/10.1007/978-3-642-12032-9_2

Schwinghammer, J., Birkedal, L., Reus, B. & Yang, H. (2009). Nested hoare triples and frame rules for higher-order store. In E. Grädel & R. Kahle (Eds.), Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings (pp. 440-454). Springer. https://doi.org/10.1007/978-3-642-04027-6_32

Schivo, S., Khurana, S., Govindaraj, K., Scholma, J., Kerkhofs, J., Zhong, L., Huang, X., van de Pol, J., Langerak, R., van Wijnen, A. J., Geris, L., Karperien, M. & Post, J. N. (2020). ECHO, the executable CHOndrocyte: A computational model to study articular chondrocytes in health and disease. Cellular Signalling, 68, Article 109471. https://doi.org/10.1016/j.cellsig.2019.109471

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

Sammler, M., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J., Dreyer, D., Garg, D. & Sewell, P. (2022). Islaris: verification of machine code against authoritative ISA semantics. In R. Jhala & I. Dillig (Eds.), PLDI 2022 - Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 825-840). Association for Computing Machinery. https://doi.org/10.1145/3519939.3523434

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

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

Rijke, E. & Spitters, B. (2016). Homotopy type theory and the formalization of mathematics. Nieuw Archief voor Wiskunde , 5/17(3), 159 - 164. http://www.cs.au.dk/~spitters/naw5-2016-17-3-159.pdf

Rijke, E., Shulman, M. & Spitters, B. (2017, Jun 27). Modalities in homotopy type theory. https://arxiv.org/abs/1706.07526

Rijke, E., Shulman, M. & Spitters, B. (2020). Modalities in homotopy type theory. Logical Methods in Computer Science, 16(1), 2:1-2:79. https://doi.org/10.23638/LMCS-16(1:2)2020

Reinhard, T., Timany, A. & Jacobs, B. (2020). A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report.

Reinhard, T., Timany, A. & Jacobs, B. (2020). A separation logic to verify termination of busy-waiting for abrupt program exit. In FTfJP 2020: Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs (pp. 26-32). Association for Computing Machinery. https://doi.org/10.1145/3427761.3428345

Reinhard, T., Timany, A. & Jacobs, B. (2020). A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit.

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

Qian, Z., Kavvos, G. A. & Birkedal, L. (2020). Client-Server Sessions in Linear Logic. arxiv.org. https://arxiv.org/abs/2010.13926

Qian, Z., Kavvos, G. A. & Birkedal, L. (2021). Client-server sessions in linear logic. Proceedings of the ACM on Programming Languages , 5(ICFP), Article 62. https://doi.org/10.1145/3473567

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

Pol, J. V. D. & Meijer, J. (2019). Synchronous or Alternating? LTL Black-Box Checking of Mealy Machines by Combining the LearnLib and LTSmin. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): The What, the How, and the Why Not? (pp. 417-430). Springer. https://doi.org/10.1007/978-3-030-22348-9_24

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)

Pichon-Pharabod, J. (2025). Synchronous Programming for Kids: A Manifesto. In S. Chiba, C. N. Klokmose & C. Gordon (Eds.), Onward! 2025 - Proceedings of the 2025 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Co-located with SPLASH 2025 (pp. 1-12). Association for Computing Machinery. https://doi.org/10.1145/3759429.3762617

Petsinis, P., Pavlogiannis, A. & Karras, P. (2023). Maximizing the Probability of Fixation in the Positional Voter Model. In B. Williams, Y. Chen & J. Neville (Eds.), AAAI-23 Technical Tracks 10 (pp. 12269-12277). Article 190493 AAAI Press. https://doi.org/10.1609/aaai.v37i10.2636126446

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

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

Petersen, R. L., Birkedal, L., Nanevski, A. & Morrisett, G. (2008). A realizability model for impredicative Hoare Type Theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4960 LNCS, pp. 337-352) https://doi.org/10.1007/978-3-540-78739-6_26

Penninckx, W., Timany, A. & Jacobs, B. (2019). Specifying i/o using abstract nested hoare triples in separation logic. In Proceedings of the 21st Workshop on Formal Techniques for Java-Like Programs, FTfJP 2019 - Co-located with ECOOP 2019 Article 5 Association for Computing Machinery. https://doi.org/10.1145/3340672.3341118

Penninckx, W., Timany, A. & Jacobs, B. (2019). Abstract I/O Specification. ArXiv. http://arxiv.org/abs/1901.10541v1

Pedersen, M. V. & Askarov, A. (2017). From Trash to Treasure: Timing-Sensitive Garbage Collection. In 2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings (pp. 693-709). Article 7958605 IEEE Computer Society Press. https://doi.org/10.1109/SP.2017.64

Pavlogiannis, A., Tkadlec, J., Chatterjee, K. & Nowak, M. A. (2018). Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory. Communications Biology, 1(1), Article 71. https://doi.org/10.1038/s42003-018-0078-7

Pavlogiannis, A., Chatterjee, K., Adlam, B. & Nowak, M. A. (2015). Cellular cooperation with shift updating and repulsion. Scientific Reports, 5, 17147. https://doi.org/10.1038/srep17147

Pavlogiannis, A., Tkadlec, J., Chatterjee, K. & Nowak, M. A. (2017). Amplification on Undirected Population Structures: Comets Beat Stars. Scientific Reports, 7(1), 82. Article 82. https://doi.org/10.1038/s41598-017-00107-w

Pavlogiannis, A. (2020). Fast, Sound, and Effectively Complete Dynamic Race Prediction. Proceedings of the ACM on Programming Languages , 4(POPL), 1-29. Article 17. https://doi.org/10.1145/3371085

Pavlogiannis, A. (2020). The Fine-Grained Complexity of Andersen's Pointer Analysis. ArXiv. https://arxiv.org/abs/2006.01491

Pavlogiannis, A., Schaumberger, N., Schmid, U. & Chatterjee, K. (2020). Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 39(11), 3981-3992. Article 9211419. https://doi.org/10.1109/TCAD.2020.3012803

Paviotti, M., Møgelberg, R. E. & Birkedal, L. (2015). A model of PCF in guarded type theory. Electronic Notes in Theoretical Computer Science, 319, 333–349. https://doi.org/10.1016/j.entcs.2015.12.020

Oortwijn, W., Huisman, M., Joosten, S. J. C. & van de Pol, J. (2020). Automated verification of parallel nested DFS. In A. Biere & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I (pp. 247-265). Springer. https://doi.org/10.1007/978-3-030-45190-5_14

Niss, H. & Birkedal, L. (Eds.) (2004). Context-aware computing: proceedings of conference on Context-aware Computing, Copenhagen, November 30, 2004. IT University of Copenhagen.

Nieto, A., Gondelman, L., Reynaud, A., Timany, A. & Birkedal, L. (2022). Modular verification of op-based CRDTs in separation logic. Proceedings of the ACM on Programming Languages , 6(OOPSLA2), 1788-1816. Article 188. https://doi.org/10.1145/3563351

Nieto, A., Daby-Seesaram, A., Gondelman, L., Timany, A. & Birkedal, L. (2023). Modular Verification of State-Based CRDTs in Separation Logic. In K. Ali & G. Salvaneschi (Eds.), 37th European Conference on Object-Oriented Programming, ECOOP 2023 Article 22 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2023.22

Nielsen, J. B. & Spitters, B. (2019). Smart Contract Interactions in Coq. (0 ed.) ArXiv.

Nielsen, J. B. & Spitters, B. (2020). Smart contract interactions in coq. In E. Sekerinski, N. Moreira, J. N. Oliveira, D. Ratiu, R. Guidotti, M. Farrell, M. Luckcuck, D. Marmsoler, J. Campos, T. Astarte, L. Gonnord, A. Cerone, L. Couto, B. Dongol, M. Kutrib, P. Monteiro & D. Delmas (Eds.), Formal Methods- FM 2019 International Workshops - Revised Selected Papers (pp. 380-391). Springer. https://doi.org/10.1007/978-3-030-54994-7_29

Nielsen, B. B. & Møller, A. (2020). Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript. In 34th European Conference on Object-Oriented Programming, ECOOP 2020 Article 16 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2020.16

Nielsen, B. B., Torp, M. T. & Møller, A. (2020). Detecting Locations in JavaScript Programs Affected by Breaking Library Changes. Proceedings of the ACM on Programming Languages , 4(OOPSLA), Article 187. https://doi.org/10.1145/3428255

Nielsen, B. B., Torp, M. T. & Møller, A. (2021). Modular call graph construction for security scanning of Node.js applications. In C. Cadar & X. Zhang (Eds.), ISSTA 2021 - Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 29-41). Association for Computing Machinery. https://doi.org/10.1145/3460319.3464836

Nielsen, B. B., Torp, M. T. & Møller, A. (2021). Semantic Patches for Adaptation of JavaScript Programs to Evolving Libraries. In Proceedings - 2021 IEEE/ACM 43rd International Conference on Software Engineering, ICSE 2021 (pp. 74-85). IEEE. https://doi.org/10.1109/ICSE43902.2021.00020

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

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

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

Displaying results 101 to 150 out of 533

Revised 05.12.2025

Marianne Dammand Iversen