Publications

Sort by: Date | Author | Title

Georges, A. L. (2023). Designing and Proving Robust Safety of Efficient Capability Machine Programs. Aarhus Universitet.

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. 111-126). IEEE. https://doi.org/10.1109/CSF57540.2023.00008

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

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

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

Hinrichsen, J. K., Bengtson, J. & Krebbers, R. (2022). ACTRIS 2.0: ASYNCHRONOUS SESSION-TYPE BASED REASONING IN SEPARATION LOGIC. Logical Methods in Computer Science, 18(2), 16:1-16:64. https://doi.org/10.46298/lmcs-18(2:16)2022

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. Advance online publication. 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 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2022.23

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

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) Schloss Dagstuhl--Leibniz-Zentrum für Informatik. https://doi.org/10.4230/OASIcs.FMBC.2022.2

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

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

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

Aagaard, F. L., Kristensen, M., Gratzer, D. & Birkedal, L. (2022). Unifying Cubical and Multimodal Type Theory. Abstract from 28th International Conference on Types for Proofs and Programs, Nantes, France. https://types22.inria.fr/files/2022/06/TYPES_2022_paper_35.pdf

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

André, É., Marinho, D. & Pol, J. V. D. (2021). A Benchmarks Library for Extended Parametric Timed Automata. In F. Loulergue & F. Wotawa (Eds.), Tests and Proofs - 15th International Conference, TAP 2021, Held as Part of STAF 2021, Proceedings: 15th International Conference, TAP 2021, Held as Part of STAF 2021, Virtual Event, June 21–22, 2021, Proceedings (pp. 39-50). Springer. https://doi.org/10.1007/978-3-030-79379-1_3

Sølvsten, S. (Producer). (2021). Adiar: An I/O-efficient implementation of Binary Decision Diagrams. Software, GitHub. https://github.com/SSoelvsten/adiar

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

Georges, A. L., Guéneau, A., Van Strydonck, T., Timany, A., Trieu, A., Devriese, D. & Birkedal, L. (2021). Cap’ ou pas cap’ ?: Preuve de programmes pour une machine à capacités en présence de code inconnu. In Journées Francophones des Langages Applicatifs 2021 Institut de Recherche en Informatique Fondamentale. https://researchportal.vub.be/en/publications/cap-ou-pas-cap-preuve-de-programmes-pour-une-machine-%C3%A0-capacit%C3%A9s-

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

Frumin, D., Krebbers, R. & Birkedal, L. (2021). Compositional non-interference for fine-grained concurrent programs. In 2021 IEEE Symposium on Security and Privacy (SP) (pp. 1416-1433). IEEE. https://doi.org/10.1109/SP40001.2021.00003

Vindum, S. F. & Birkedal, L. (2021). Contextual refinement of the Michael-Scott queue (proof pearl). In C. Hriţcu & A. Popescu (Eds.), CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 76-90). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439930

Gondelman, L., Gregersen, S. O., Nieto, A., Timany, A. & Birkedal, L. (2021). Distributed causal memory: Modular specification and verification in higher-order distributed separation logic. Proceedings of the ACM on Programming Languages, 5(POPL), Article 42. https://doi.org/10.1145/3434323

Georges, A. L., Guéneau, A., Van Strydonck, T., Timany, A., Trieu, A., Huyghebaert, S., Devriese, D. & Birkedal, L. (2021). Efficient and provable local capability revocation using uninitialized capabilities. Proceedings of the ACM on Programming Languages, 5(POPL), Article 6. https://doi.org/10.1145/3434287

Annenkov, D., Milo, M., Nielsen, J. B. & Spitters, B. (2021). Extracting smart contracts tested and verified in Coq. In C. Hritcu & A. Popescu (Eds.), CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021 (pp. 105-121). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439934

Thomsen, S. E. & Spitters, B. (2021). Formalizing Nakamoto-Style Proof of Stake. In Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021 IEEE. https://doi.org/10.1109/CSF51468.2021.00042

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

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

Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Katsumata, S. Y. & Sato, T. (2021). Higher-order probabilistic adversarial computations: categorical semantics and program logics. Proceedings of the ACM on Programming Languages, 5(ICFP), Article 93. https://doi.org/10.1145/3473598

André, É., Arias, J., Petrucci, L. & Pol, J. V. D. (2021). Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata. In J. F. Groote & K. G. Larsen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part I (pp. 311-329). Springer. https://doi.org/10.1007/978-3-030-72016-2_17

Gregersen, S. O., Bay, J., Timany, A. & Birkedal, L. (2021). Mechanized logical relations for termination-insensitive noninterference. Proceedings of the ACM on Programming Languages, 5(POPL), Article 10. https://doi.org/10.1145/3434291

Gratzer, D., Kavvos, G. A., Nuyts, A. & Birkedal, L. (2021). Multimodal Dependent Type Theory. Logical Methods in Computer Science, 17(3), Article 11. https://doi.org/10.46298/lmcs-17(3:11)2021

Ahmadpanah, M. M., Askarov, A. & Sabelfeld, A. (2021). Nontransitive policies transpiled. In 2021 IEEE European Symposium on Security and Privacy (EuroS&P) (pp. 543-561). IEEE. https://doi.org/10.1109/EuroSP51992.2021.00043

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

Displaying results 1 to 50 out of 274

Revised 17.04.2023

Sofia Hedegaard Rasmussen