Publications

Sortér efter: Dato | Forfatter | Titel

Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J. & Birkedal, L. (2024). Almost-Sure Termination by Guarded Refinement. Proceedings of the ACM on Programming Languages , 8(ICFP), 203-233. Artikel 243. https://doi.org/10.1145/3674632

Hammond, A., Liu, Z., Pérami, T., Sewell, P., Birkedal, L. & Pichon-Pharabod, J. (2024). An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. Proceedings of the ACM on Programming Languages , 8, 604-637. Artikel 21. https://doi.org/10.1145/3632863

Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J. & Birkedal, L. (2024). Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proceedings of the ACM on Programming Languages , 8(POPL), Artikel 26. https://doi.org/10.1145/3632868

Georges, A. L., Guéneau, A., Van Strydonck, T., Timany, A., Trieu, A., Devriese, D. & Birkedal, L. (2024). Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. Journal of the ACM, 71(1), Artikel 3. https://doi.org/10.1145/3623510

Aguirre, A., Haselwarter, P. G., De Medeiros, M., Li, K. H., Gregersen, S. O., Tassarotti, J. & Birkedal, L. (2024). Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. Proceedings of the ACM on Programming Languages , 8, Artikel 246. https://doi.org/10.1145/3674635

Jakobsen, A. B., Jørgensen, R. S. M., van de Pol, J. & Pavlogiannis, A. (2024). Fast Symbolic Computation of Bottom SCCs. I B. Finkbeiner & L. Kovács (red.), Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024 (s. 110-128). Springer. https://doi.org/10.1007/978-3-031-57256-2_6

Frumin, D., Timany, A. & Birkedal, L. (2024). Modular Denotational Semantics for Effects with Guarded Interaction Trees. Proceedings of the ACM on Programming Languages , 8(POPL), Artikel 12. https://doi.org/10.1145/3632854

Dahlsen-Jensen, M. B., Fievet, B., Petrucci, L. & de Pol, J. V. (2024). On-The-Fly Algorithm for Reachability in Parametric Timed Games. I B. Finkbeiner & L. Kovács (red.), Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings (s. 194-212). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-57256-2_10

Shaik, I. & Van de Pol, J. (2024). Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits. I S. Chakraborty & J.-H. R. Jiang (red.), 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024 Artikel 26 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SAT.2024.26

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

Haselwarter, P. G., Hvass, B. S., Hansen, L. L., Winterhalter, T., Hriţcu, C. & Spitters, B. (2024). The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. I A. Timany, D. Traytel, B. Pientka & S. Blazy (red.), CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (s. 30-44). Association for Computing Machinery. https://doi.org/10.1145/3636501.3636961

Timany, A., Guéneau, A. & Birkedal, L. (2024). The Logical Essence of Well-Bracketed Control Flow. Proceedings of the ACM on Programming Languages , 8(POPL), 575-603. https://doi.org/10.1145/3632862

Sterling, J., Gratzer, D. & Birkedal, L. (2024). Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. I A. Murano & A. Silva (red.), 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024 Artikel 47 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2024.47

Pientka, B., Blazy, S., Traytel, D. & Timany, A. (2024). Welcome from the Chairs. I CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024 (s. iii-iv)

Aagaard, F. L., Sterling, J. & Birkedal, L. (2023). A denotationally-based program logic for higher-order store. Electronic Notes in Theorical Informatics and Computer Science, 3. https://doi.org/10.46298/entics.12232

Sølvsten, S. & van de Pol, J. (2023). Adiar 1.1: Zero-Suppressed Decision Diagrams in External Memory. I K. Y. Rozier & S. Chaudhuri (red.), NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings (s. 464-471). Springer. https://doi.org/10.1007/978-3-031-33170-1_28

Gleirscher, M., van de Pol, J. & Woodcock, J. (2023). A manifesto for applicable formal methods. Software and Systems Modeling, 22(6), 1737-1749. https://doi.org/10.1007/s10270-023-01124-2

Larsen, C. A., Schmidt, S. M., Steensgaard, J., Jakobsen, A. B., Pol, J. V. D. & Pavlogiannis, A. (2023). A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. I S. Sankaranarayanan & N. Sharygina (red.), Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II (s. 353-371). Springer. https://doi.org/10.1007/978-3-031-30820-8_22

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

Madsen, M., Van De Pol, J. & Henriksen, T. (2023). Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems. Proceedings of the ACM on Programming Languages , 7(OOPSLA2), 516–543. Artikel 240. https://doi.org/10.1145/3622816

Aranha, D. F., Hvass, B. S., Spitters, B. & Tibouchi, M. (2023). Faster constant-time evaluation of the Kronecker symbol with application to elliptic curve hashing. I CCS'23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (s. 3228-3238). Association for Computing Machinery. https://doi.org/10.1145/3576915.3616597

Haselwarter, P. G. & Bauer, A. (2023). Finitary Type Theories With and Without Contexts. Journal of Automated Reasoning, 67(4), Artikel 36. https://doi.org/10.1007/s10817-023-09678-y

Nielsen, E. H., Annenkov, D. & Spitters, B. (2023). Formalising Decentralised Exchanges in Coq. I R. Krebbers, D. Traytel, B. Pientka & S. Zdancewic (red.), CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (s. 290-302). Association for Computing Machinery. https://doi.org/10.1145/3573105.3575685

Hvass, B. S., Aranha, D. F. & Spitters, B. (2023). High-assurance field inversion for curve-based cryptography. I 2023 IEEE 36th Computer Security Foundations Symposium (CSF) (s. 552-567). IEEE. https://doi.org/10.1109/CSF57540.2023.00008

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

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, Artikel 151. https://doi.org/10.1145/3591265

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. Artikel 247. https://doi.org/10.1145/3622823

Stassen, P. J. A., Gratzer, D. & Birkedal, L. (2023). mitten: A Flexible Multimodal Proof Assistant. I D. Kesner & P.-M. Pedrot (red.), 28th International Conference on Types for Proofs and Programs Artikel 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. I K. Ali & G. Salvaneschi (red.), 37th European Conference on Object-Oriented Programming, ECOOP 2023 Artikel 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. Afhandling præsenteret på 36th IEEE Computer Security Foundations Symposium, Dubrovnik, Kroatien.

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

Sølvsten, S. & van de Pol, J. (2023). Predicting Memory Demands of BDD Operations using Maximum Graph Cuts. I É. André & J. Sun (red.), Automated technology for verification and analysis: Part II (s. 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. I K. Ali & G. Salvaneschi (red.), 37th European Conference on Object-Oriented Programming (ECOOP 2023) Artikel 18 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2023.18

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. Artikel 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. Artikel 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. Artikel 2. https://doi.org/10.1145/3571195

Gratzer, D. (2023). Syntax and semantics of modal type theory. Aarhus University.

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

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. I D. Fisman & G. Rosu (red.), 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 (s. 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, Artikel 101456. https://doi.org/10.1016/j.is.2019.101456

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

Shaik, I. & van de Pol, J. (2022). Classical Planning as QBF without Grounding. I A. Kumar, S. Thiebaux, P. Varakantham & W. Yeoh (red.), Proceedings of the 32nd International Conference on Automated Planning and Scheduling, ICAPS 2022 (s. 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. I S. Bogomolov & D. Parker (red.), Formal Modeling and Analysis of Timed Systems. FORMATS 2022 (s. 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. I T. Margaria & B. Steffen (red.), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings (s. 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), Artikel 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

Viser resultater 1 til 50 ud af 309

Næste

Revideret 17.04.2023

Sofia Hedegaard Rasmussen