Publications

Sort by: Date | Author | Title

Sølvsten, S., van de Pol, J., Jakobsen, A. B. & Thomasen, M. W. B. (2021). Efficient Binary Decision Diagram Manipulation in External Memory. ArXiv. https://doi.org/10.48550/arXiv.2104.12101

Sølvsten, S., van de Pol, J., Jakobsen, A. B., Rysgaard, C. M., Carstensen, E. F. & Thomasen, M. W. B. (2021). Adiar: An I/O-efficient implementation of Decision Diagrams. Software, GitHub. https://doi.org/10.5281/zenodo.4718218

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

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

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

Sølvsten, S., Rysgaard, C. M. & van de Pol, J. (2025). Random Access on Narrow Decision Diagrams in External Memory. In T. Neele & A. Wijs (Eds.), Model Checking Software: 30th International Symposium, SPIN 2024, Luxembourg City, Luxembourg, April 8–9, 2024, Proceedings (pp. 137–145). Springer. https://doi.org/10.1007/978-3-031-66149-5_7

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

Sølvsten, S. & van de Pol, J. (2025). Symbolic Model Checking in External Memory. ArXiv. https://doi.org/10.48550/arXiv.2505.11229

Skorstensgaard, L., Devriese, D. & Birkedal, L. (2021). StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Journal of Functional Programming, 31, Article e9. https://doi.org/10.1017/S095679682100006X

Skorstengaard, L., Devriese, D. & Birkedal, L. (2018). Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. In A. Ahmed (Ed.), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (Vol. 10801, pp. 475-501). Springer VS. https://doi.org/10.1007/978-3-319-89884-1_17

Skorstengaard, L., Devriese, D. & Birkedal, L. (2019). Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. A C M Transactions on Programming Languages and Systems, 41(4), Article 5. https://doi.org/10.1145/3363519

Skorstengaard, L., Devriese, D. & Birkedal, L. (2019). StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities. Proceedings of the ACM on Programming Languages , 3(POPL), Article 19. https://doi.org/10.1145/3290332

Skorstengaard, L., Devriese, D. & Birkedal, L. (2019). Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. ACM Transactions on Programming Languages and Systems, 42(1), Article 5. https://doi.org/10.1145/3363519

Sieczkowski, F., Svendsen, K., Birkedal, L. & Pichon-Pharabod, J. (2015). A separation logic for fictional sequential consistency. In J. Vitek (Ed.), Programming Languages and Systems : 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 (pp. 736-761). Springer. https://doi.org/10.1007/978-3-662-46669-8_30

Sieczkowski, F., Bizjak, A. & Birkedal, L. (2015). ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. In C. Urban & X. Zhang (Eds.), Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (pp. 375-390). Springer. https://doi.org/10.1007/978-3-319-22102-1_25

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

Sidorenco, N., Oechsner, S. & Spitters, B. (2021). Formal security analysis of MPC-in-the-head zero-knowledge protocols. In Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021 (pp. 607-620). IEEE. https://doi.org/10.1109/CSF51468.2021.00050

Shaik, I. & Pol, J. V. D. (2021). Classical Planning as QBF without Grounding (extended version). (pp. 1-17). CoRR https://arxiv.org/abs/2106.10138

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

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

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

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

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

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

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

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

Schwinghammer, J., Birkedal, L. & Støvring, K. (2011). A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces. In M. Hofmann (Ed.), Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings (pp. 305-319). Springer. https://doi.org/10.1007/978-3-642-19805-2_21

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

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

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.

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

Rakotonirina, I., Ambrona, M., Aguirre, A. & Barthe, G. (2022). Symbolic Synthesis of Indifferentiability Attacks. In ASIA CCS 2022 - Proceedings of the 2022 ACM Asia Conference on Computer and Communications Security (pp. 667-681). Association for Computing Machinery. https://doi.org/10.1145/3488932.3497759

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)

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

Displaying results 51 to 100 out of 345

Revised 17.04.2023

Sofia Hedegaard Rasmussen