Publications

Sort by: Date | Author | Title

Gleirscher, M., Pol, J. V. D. & Woodcock, J. (Eds.) (2021). Proceedings First Workshop on Applicable Formal Methods. Electronic Proceedings in Theoretical Computer Science https://doi.org/10.4204/EPTCS.349

Timany, A. & Birkedal, L. (2021). Reasoning about monotonicity in separation logic. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21) (pp. 91-104). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439931

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

Frumin, D., Krebbers, R. & Birkedal, L. (2021). ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. Logical Methods in Computer Science, 17(3), Article 9. https://doi.org/10.46298/lmcs-17(3:9)2021

Abate, C., Haselwarter, P. G., Rivas, E., Muylder, A. V., Winterhalter, T., Hritcu, C., Maillard, K. & Spitters, B. (2021). SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. (pp. 397). Cryptology ePrint Archive. https://eprint.iacr.org/2021/397

Abate, C., Haselwarter, P. G., Rivas, E., Muylder, A. V., Winterhalter, T., Hriţcu, C., Maillard, K. & Spitters, B. (2021). SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. In Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021 IEEE. https://doi.org/10.1109/CSF51468.2021.00048

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

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

Mathiasen, A. A. & Pavlogiannis, A. (2021). The Fine-Grained and Parallel Complexity of Andersen’s Pointer Analysis. Proceedings of the ACM on Programming Languages , 5(POPL), Article 34. https://doi.org/10.1145/3434315

Birkedal, L., Dinsdale-Young, T., Guéneau, A., Jaber, G., Svendsen, K. & Tzevelekos, N. (2021). Theorems for free from separation logic specifications. Proceedings of the ACM on Programming Languages , 5(ICFP), Article 81. https://doi.org/10.1145/3473586

Blaabjerg, J. F. & Askarov, A. (2021). Towards Language-Based Mitigation of Traffic Analysis Attacks. Paper presented at 34th IEEE Computer Security Foundations Symposium, Online, United States.

Spies, S., Gäher, L., Gratzer, D., Tassarotti, J., Krebbers, R., Dreyer, D. & Birkedal, L. (2021). Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. In S. N. Freund & E. Yahav (Eds.), PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 80-95). Association for Computing Machinery. https://doi.org/10.1145/3453483.3454031

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

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

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

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: Technical Report.

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

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

Wimmer, S., Herbreteau, F. & van de Pol, J. (2020). Certifying Emptiness of Timed Büchi Automata. In N. Bertrand & N. Jansen (Eds.), Formal Modeling and Analysis of Timed Systems : 18th International Conference, FORMATS 2020 (pp. 58-75). Springer. https://doi.org/10.1007/978-3-030-57628-8_4

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

Annenkov, D., Nielsen, J. B. & Spitters, B. (2020). ConCert: A Smart Contract Certification Framework in Coq. (pp. 215-228). arxiv.org. https://doi.org/10.1145/3372885.3373829

Annenkov, D., Botsch Nielsen, J. & Spitters, B. (2020). ConCert: A smart contract certification framework in Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20-21, 2020, New Orleans, LA, USA (pp. 215-228). Association for Computing Machinery. https://doi.org/10.1145/3372885.3373829

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

Birkedal, L. (2020). Editorial message. Proceedings of the ACM on Programming Languages , 4(POPL).

Thomsen, S. E. & Spitters, B. (2020). Formalizing Nakamoto-Style Proof of Stake.

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

Abel, A., Cockx, J., Devriese, D., Timany, A. & Wadler, P. (2020). Leibniz equality is isomorphic to Martin-Löf identity, parametrically. Journal of Functional Programming, 30, Article e17. https://doi.org/10.1017/S0956796820000155

Birkedal, L., Clouston, R., Mannaa, B., Ejlers Møgelberg, R., Pitts, A. M. & Spitters, B. (2020). Modal dependent type theory and dependent right adjoints. Mathematical Structures in Computer Science, 30(2), 118-138. https://doi.org/10.1017/S0960129519000197

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

Gratzer, D., Kavvos, G. A., Nuyts, A. & Birkedal, L. (2020). Multimodal Dependent Type Theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 (pp. 492-506). Article 3394736 Association for Computing Machinery. https://doi.org/10.1145/3373718.3394736

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

Hansen, K. A. & Sølvsten, S. C. (2020). ∃R-completeness of stationary nash equilibria in perfect information stochastic games. In J. Esparza & D. Král (Eds.), 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020 (pp. 45:1-45:15). Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.MFCS.2020.45

Bay, J. & Askarov, A. (2020). Reconciling progress-insensitive noninterference and declassification. In 2020 IEEE 33rd Computer Security Foundations Symposium (CSF) (pp. 95-106). IEEE. https://doi.org/10.1109/CSF49147.2020.00015

Frumin, D., Krebbers, R. & Birkedal, L. (2020). ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. arxiv.org. https://arxiv.org/abs/2006.13635

Giarrusso, P. G., Stefanesco, L., Timany, A., Birkedal, L. & Krebbers, R. (2020). Scala step-by-step: Soundness for DOT with step-indexed logical relations in Iris. Proceedings of the ACM on Programming Languages , 4(ICFP), Article 114. https://doi.org/10.1145/3408996

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

Garavel, H., ter Beek, M. H. & van de Pol, J. (2020). The 2020 Expert Survey on Formal Methods. In M. H. ter Beek & D. Nickovic (Eds.), Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings: FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings (pp. 3-69). Springer. https://doi.org/10.1007/978-3-030-58298-2_1

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

Blatchley Hansen, A., Eskilden, M. & Nielsen, E. H. (2020). Toolchain for Timing Leakage Analysis of NIST Lightweight Crypto Candidates. Abstract from NIST Lightweight Cryptography Workshop 2020. https://csrc.nist.gov/CSRC/media/Events/lightweight-cryptography-workshop-2020/documents/papers/toolchain-timing-leakage-lwc2020.pdf

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

Gregersen, S. O., Thomsen, S. E. & Askarov, A. (2019). A Dependently Typed Library for Static Information-Flow Control in IDRIS. In F. Nielson & D. Sands (Eds.), Principles of Security and Trust: 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 51-75). Springer. https://doi.org/10.1007/978-3-030-17138-4_3

van de Pol, J. (2019). Concurrent algorithms and data structures for model checking. In W. Fokkink & R. van Glabbeek (Eds.), 30th International Conference on Concurrency Theory, CONCUR 2019 Article 4 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2019.4

Van Der Berg, F. I. & Van De Pol, J. (2019). Concurrent chaining hash maps for software model checking. In C. Barrett & J. Yang (Eds.), Proceedings of the 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019 (pp. 46-54). Article 8894279 IEEE. https://doi.org/10.23919/FMCAD.2019.8894279

Sterling, J., Angiuli, C. & Gratzer, D. (2019). Cubical syntax for reflection-free extensional equality. In H. Geuvers (Ed.), 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019 Article 31 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2019.31

Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2019). Guarded Cubical Type Theory. Journal of Automated Reasoning, 63(2), 211-253. https://doi.org/10.1007/s10817-018-9471-7, https://doi.org/10.1007/s10817-018-9471-7

Gratzer, D., Sterling, J. & Birkedal, L. (2019). Implementing a modal dependent type theory. Proceedings of the ACM on Programming Languages , 3(ICFP), 1-29. Article 107. https://doi.org/10.1145/3341711

Bizjak, A., Gratzer, D., Krebbers, R. & Birkedal, L. (2019). Iron: managing obligations in higher-order concurrent separation logic. Proceedings of the ACM on Programming Languages , 3(POPL), 1-30. Article 65. https://doi.org/10.1145/3290378

Displaying results 101 to 150 out of 336

Revised 17.04.2023

Sofia Hedegaard Rasmussen