Find

For students
For PhDs
For employees

Department of Computer Science

Publications

Sort by: Date | Author | Title

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

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

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

Stassen, P. J. A., Gratzer, D. & Birkedal, L. (2023). mitten: A Flexible Multimodal Proof Assistant. In D. Kesner & P.-M. Pedrot (Eds.), 28th International Conference on Types for Proofs and Programs Article 6 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.TYPES.2022.6

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

Blaabjerg, J. F. & Askarov, A. (2023). OblivIO: Securing reactive programs by oblivious execution with bounded traffic overheads. Paper presented at 36th IEEE Computer Security Foundations Symposium, Dubrovnik, Croatia.

Shaik, I. & van de Pol, J. (2023). Optimal Layout Synthesis for Quantum Circuits as Classical Planning. In 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD) IEEE. https://doi.org/10.1109/ICCAD57390.2023.10323924

Tunç, H. C., Abdulla, P. A., Chakraborty, S., Krishna, S., Mathur, U. & Pavlogiannis, A. (2023). Optimal Reads-From Consistency Checking for C11-Style Memory Models. Proceedings of the ACM on Programming Languages , 7(PLDI), 761–785. Article 137. https://doi.org/10.1145/3591251

Sølvsten, S. & van de Pol, J. (2023). Predicting Memory Demands of BDD Operations using Maximum Graph Cuts. In É. André & J. Sun (Eds.), Automated technology for verification and analysis: Part II (pp. 72-92). Springer. https://doi.org/10.1007/978-3-031-45332-8_4

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., 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

Tunç, H. C., Mathur, U., Pavlogiannis, A. & Viswanathan, M. (2023). Sound Dynamic Deadlock Prediction in Linear Time. Proceedings of the ACM on Programming Languages , 7, 1733-1758. https://doi.org/10.1145/3591291

Vindum, S. F. & Birkedal, L. (2023). Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory. Proceedings of the ACM on Programming Languages , 7(OOPSLA2), 632-657. Article 244. https://doi.org/10.1145/3622820

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

Aguirre, A. & Birkedal, L. (2023). Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. Proceedings of the ACM on Programming Languages , 7, 33-60. Article 2. https://doi.org/10.1145/3571195

Gratzer, D. (2023). Syntax and semantics of modal type theory. [PhD dissertation, Aarhus University]. Aarhus Universitet.

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

Shaik, I., Heisinger, M., Seidl, M. & Pol, J. V. D. (2023). Validation of QBF Encodings with Winning Strategies. Leibniz International Proceedings in Informatics, 271. https://doi.org/10.4230/LIPIcs.SAT.2023.24

Gondelman, L., Hinrichsen, J. K., Pereira, M., Timany, A. & Birkedal, L. (2023). Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. Proceedings of the ACM on Programming Languages , 7(ICFP), 847-877. Article 217. https://doi.org/10.1145/3607859

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

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

Sterling, J., Angiuli, C. & Gratzer, D. (2022). A cubical language for bishop sets. Logical Methods in Computer Science, 18(1), 43:1-43:80. https://doi.org/10.46298/LMCS-18(1:43)2022

Sølvsten, S. C., de Pol, J. V., Jakobsen, A. B. & Thomasen, M. W. B. (2022). Adiar Binary Decision Diagrams in External Memory. In D. Fisman & G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings (pp. 295-313). Springer. https://doi.org/10.1007/978-3-030-99527-0_16

Bloemen, V., Zelst, S. V., Aalst, W. V. D., Dongen, B. V. & Pol, J. V. D. (2022). Aligning observed and modelled behaviour by maximizing synchronous moves and using milestones. Information Systems, 103, Article 101456. https://doi.org/10.1016/j.is.2019.101456

Gratzer, D. & Birkedal, L. (2022). A Stratified Approach to Löb Induction. In A. P. Felty (Ed.), 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022 Article 23 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2022.23

Mathur, U., Pavlogiannis, A., Tunc, H. C. & Viswanathan, M. (2022). A Tree Clock Data Structure for Causal Orderings in Concurrent Executions. In B. Falsafi, M. Ferdman, S. Lu & T. F. Wenisch (Eds.), ASPLOS 2022 - Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (pp. 710-725). Association for Computing Machinery. https://doi.org/10.1145/3503222.3507734

Shaik, I. & van de Pol, J. (2022). Classical Planning as QBF without Grounding. In A. Kumar, S. Thiebaux, P. Varakantham & W. Yeoh (Eds.), Proceedings of the 32nd International Conference on Automated Planning and Scheduling, ICAPS 2022 (pp. 329-337). AAAI Press. https://doi.org/10.1609/icaps.v32i1.19817

Veileborg, O. H., Saioc, G.-V. & Møller, A. (2022). Detecting Blocking Errors in Go Programs using Localized Abstract Interpretation. In iWOAR 2022 - 7th International Workshop on Sensor-Based Activity Recognition and Artificial Intelligence, Proceedings (pp. 1-12). Article 32 Association for Computing Machinery. https://doi.org/10.1145/3551349.3561154

Ahmadi, A., Daliri, M., Goharshady, A. K. & Pavlogiannis, A. (2022). Efficient approximations for cache-conscious data placement. In R. Jhala & I. Dillig (Eds.), Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 857-871). Association for Computing Machinery. https://doi.org/10.1145/3519939.3523436

André, É., Marinho, D., Petrucci, L. & van de Pol, J. (2022). Efficient Convex Zone Merging in Parametric Timed Automata. In S. Bogomolov & D. Parker (Eds.), Formal Modeling and Analysis of Timed Systems. FORMATS 2022 (pp. 200-218). Springer. https://doi.org/10.1007/978-3-031-15839-1_12

van de Pol, J. (2022). Exploring a Parallel SCC Algorithm: Using TLA ⁺ and the TLC Model Checker. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings (pp. 535-555). Springer. https://doi.org/10.1007/978-3-031-19849-6_30

Annenkov, D., Milo, M., Nielsen, J. B. & Spitters, B. A. S. (2022). Extracting functional programs from Coq, in Coq. Journal of Functional Programming, 32(5), Article e11. https://doi.org/10.1017/S0956796822000077

Milo, M., Nielsen, E. H., Annenkov, D. & Spitters, B. (2022). Finding smart contract vulnerabilities with ConCert's property-based testing framework. FMBC: Formal Methods for Blockchains https://doi.org/10.48550/arXiv.2208.00758

Milo, M., Nielsen, E. H., Annenkov, D. & Spitters, B. (2022). Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework. In Z. Dargaye & C. Schneidewind (Eds.), 4th International Workshop on Formal Methods for Blockchains (FMBC 2022) Dagstuhl Publishing. https://doi.org/10.4230/OASIcs.FMBC.2022.2

Brendborg, J., Karras, P., Pavlogiannis, A., Rasmussen, A. U. & Tkadlec, J. (2022). Fixation Maximization in the Positional Moran Process. Proceedings of the AAAI Conference on Artificial Intelligence, 36(9, AAAI Technical Track on Multiagent Systems), 9304-9312. https://doi.org/10.1609/aaai.v36i9.21160

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

Svoboda, J., Tkadlec, J., Pavlogiannis, A., Chatterjee, K. & Nowak, M. A. (2022). Infection dynamics of COVID-19 virus under lockdown and reopening. Scientific Reports, 12, Article 1526. https://doi.org/10.1038/s41598-022-05333-5

Durocher, L., Karras, P., Pavlogiannis, A. & Tkadlec, J. (2022). Invasion Dynamics in the Biased Voter Process. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) (pp. 265-271). IJCAI Organization. https://doi.org/10.24963/ijcai.2022/38

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

Spies, S., Gäher, L., Tassarotti, J., Jung, R., Krebbers, R., Birkedal, L. & Dreyer, D. (2022). Later credits: resourceful reasoning for the later modality. Proceedings of the ACM on Programming Languages , 6(ICFP), Article 100. https://doi.org/10.1145/3547631

Georges, A. L., Trieu, A. & Birkedal, L. (2022). Le temps des cerises: Efficient temporal stack safety on capability machines using directed capabilities. Proceedings of the ACM on Programming Languages , 6(OOPSLA1), Article 74. https://doi.org/10.1145/3527318

Vindum, S. F., Frumin, D. & Birkedal, L. (2022). Mechanized Verification of a Fine-Grained Concurrent Queue from Meta s Folly Library. In A. Popescu & S. Zdancewic (Eds.), CPP 2022 : Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022 (pp. 100-115). Association for Computing Machinery. https://doi.org/10.1145/3497775.3503689

Gratzer, D., Cavallo, E., Kavvos, G. A., Guatto, A. & Birkedal, L. (2022). Modalities and Parametric Adjoints. ACM Transactions on Computational Logic, 23(3), Article 18. https://doi.org/10.1145/3514241

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

Daniel, G. (2022). Normalization for Multimodal Type Theory. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 Article 2 Association for Computing Machinery. https://doi.org/10.1145/3531130.3532398

Strydonck, T. V., Georges, A. L., Guéneau, A., Trieu, A., Timany, A., Piessens, F., Birkedal, L. & Devriese, D. (2022). Proving full-system security properties under multiple attacker models on capability machines. In Proceedings - 2022 IEEE 35th Computer Security Foundations Symposium, CSF 2022 (pp. 80-95). IEEE. https://doi.org/10.1109/CSF54842.2022.9919645

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

Ganardi, M., Majumdar, R., Pavlogiannis, A., Schütze, L. & Zetzsche, G. (2022). Reachability in Bidirected Pushdown VASS. In M. Bojanczyk, E. Merelli & D. P. Woodruff (Eds.), 49th EATCS International Conference on Automata, Languages, and Programming, ICALP 2022 Article 124 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ICALP.2022.124

Seisenberger, M., ter Beek, M. H., Fan, X., Ferrari, A., Haxthausen, A. E., James, P., Lawrence, A., Luttik, B., van de Pol, J. & Wimmer, S. (2022). Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Practice - 11th International Symposium, ISoLA 2022, Proceedings (pp. 246-268). Springer. https://doi.org/10.1007/978-3-031-19762-8_20

Chatterjee, K., Svoboda, J., Žikelić, Đ., Pavlogiannis, A. & Tkadlec, J. (2022). Social balance on networks: Local minima and best-edge dynamics. Physical Review E, 106(3), Article 034321. https://doi.org/10.1103/PhysRevE.106.034321

Displaying results 101 to 150 out of 545

3

Revised 05.12.2025

-

Marianne Dammand Iversen