Publications HAL de la structure epicure 2023
Journal articles
titre Formally Verified Native Code Generation in an Effectful JIT – or: Turning the CompCert Backend into a Formally Verified JIT Compiler auteur Aurèle Barrière, Sandrine Blazy, David Pichardie article Proceedings of the ACM on Programming Languages , 2023, pp.1-28. ⟨10.1145/3571202⟩ Accès au texte intégral et bibtex titre The Geometry of Causality auteur Simon Castellan, Pierre Clairambault article Proceedings of the ACM on Programming Languages , In press, pp.1-70Accès au texte intégral et bibtex Conference papers
titre Type-directed Program Transformation for Constant-Time Enforcement auteur Frédéric Besson, Thomas Jensen, Gautier Raimondi article PPDP 2023 – International Symposium on Principles and Practice of Declarative Programming , Oct 2023, Lisboa, Portugal. pp.1-13, ⟨10.1145/3610612.3610618⟩ Accès au texte intégral et bibtex titre Deriving Abstract Interpreters from Skeletal Semantics auteur Thomas Jensen, Vincent Rébiscoul, Alan Schmitt article EXPRESS/SOS 2023 – 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantics , Sep 2023, Antwerp, Belgium. pp.97-113, ⟨10.4204/EPTCS.387.8⟩ Accès au texte intégral et bibtex titre The Design and Implementation of an Abstract Interpreter for OCaml Programs auteur Benoît Montagu article ML Family 2023 – Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop , Sep 2023, Seattle, Washington, United States. pp.1-4Accès au texte intégral et bibtex titre Work in Progress: Thwarting Timing Attacks in Microcontrollers using Fine-grained Hardware Protections auteur Nicolas Gaudin, Jean-Loup Hatchikian-Houdot, Frédéric Besson, Pascal Cotret, Gogniat Guy, Guillaume Hiet, Vianney Lapotre, Pierre Wilke article SILM 2023 – Workshop on the Security of Software / Hardware Interfaces , Jul 2023, Delft, Netherlands. pp.1-7Accès au texte intégral et bibtex titre Back to the trees: Identifying plants with Human Intelligence auteur Simon Castellan, Jos Käfer, Eric Tannier article LIMITS 2023 – Ninth Workshop on Computing within Limits , Jun 2023, Virtual, France. pp.1-11, ⟨10.21428/bf6fb269.265c52ce⟩ Accès au texte intégral et bibtex titre Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures auteur Théo Losekoot, Thomas Genet, Thomas Jensen article FSCD 2023 – 8th International Conference on Formal Structures for Computation and Deduction , Jun 2023, Rome, Italy. pp.1-21, ⟨10.4230/LIPIcs.FSCD.2023.7⟩ Accès au texte intégral et bibtex titre WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms auteur Lorenzo Veronese, Benjamin Farinier, Pedro Bernardo, Mauro Tempesta, Marco Squarcina, Matteo Maffei article SP 2023 – 44th IEEE Symposium on Security and Privacy , May 2023, San Francisco, United States. pp.2761-2779, ⟨10.1109/SP46215.2023.10179465⟩ Accès au texte intégral et bibtex titre Building CFA for λ-calculus from Skeletal Semantics auteur Thomas Jensen, Vincent Rébiscoul, Alan Schmitt article JFLA 2023 – 34èmes Journées Francophones des Langages Applicatifs , Jan 2023, Praz-sur-Arly, France. pp.152-171Accès au texte intégral et bibtex titre Necro ML: Kit de Nécromancie auteur Louis Noizet, Alan Schmitt article JFLA 2023 – 34èmes Journées Francophones des Langages Applicatifs , Jan 2023, Praz-sur-Arly, France. pp.296-298Accès au texte intégral et bibtex titre Mechanised Semantics for Gated Static Single Assignment auteur Yann Herklotz, Delphine Demange, Sandrine Blazy article CPP 2023 – 12th ACM SIGPLAN International Conference on Certified Programs and Proofs , Jan 2023, Boston, United States. ⟨10.1145/3573105.3575681⟩ Accès au bibtex Book sections
titre The Mays and Musts of Concurrent Strategies auteur Simon Castellan, Pierre Clairambault, Glynn Winskel article Samson Abramsky on Logic and Structure in Computer Science and Beyond , 25, Springer International Publishing, pp.327-361, 2023, Outstanding Contributions to Logic, ⟨10.1007/978-3-031-24117-8_9⟩ Accès au texte intégral et bibtex Proceedings
titre JFLA 2023 – 34èmes Journées Francophones des Langages Applicatifs auteur Timothy Bourke, Delphine Demange article pp.1-308, 2023, Journées Francophones des Langages Applicatifs Accès au texte intégral et bibtex Reports
titre Lifting Numeric Relational Domains to Algebraic Data Types (extended version) auteur Santiago Bautista, Thomas Jensen, Benoît Montagu article [Research Report] Centre Inria de l’Université de Rennes; Univ Rennes. 2023 Accès au texte intégral et bibtex 2022
Conference papers
titre Lifting Numeric Relational Domains to Algebraic Data Types auteur Santiago Bautista, Thomas Jensen, Benoît Montagu article SAS 2022 – 29th International Symposium on Static Analysis , Dec 2022, Auckland, New Zealand. pp.104-134, ⟨10.1007/978-3-031-22308-2_6⟩ Accès au texte intégral et bibtex titre Femto-Containers: Lightweight Virtualization and Fault Isolation For Small Software Functions on Low-Power IoT Microcontrollers auteur Koen Zandberg, Emmanuel Baccelli, Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin article Middleware 2022 – 23rd ACM/IFIP International Conference Middleware , Nov 2022, Quebec, Canada. pp.1-12, ⟨10.1145/3528535.3565242⟩ Accès au texte intégral et bibtex titre Certified Derivation of Small-Step From Big-Step Skeletal Semantics auteur Guillaume Ambal, Sergueï Lenglet, Alan Schmitt, Camille Noûs article PPDP 2022 – 24th International Symposium on Principles and Practice of Declarative Programming , Sep 2022, Tbilisi, Georgia. pp.1-48, ⟨10.1145/3551357.3551384⟩ Accès au texte intégral et bibtex titre A Faithful Description of ECMAScript Algorithms auteur Adam Khayam, Louis Noizet, Alan Schmitt article PPDP 2022 – 24th International Symposium on Principles and Practice of Declarative Programming , Sep 2022, Tbilisi, Georgia. pp.1-14, ⟨10.1145/3551357.3551381⟩ Accès au texte intégral et bibtex titre Non-Deterministic Abstract Machines auteur Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt article CONCUR 2022 – 33rd International Conference
on Concurrency Theory , Sep 2022, Varsovie, Poland. pp.1-24, ⟨10.4230/LIPIcs.CONCUR.2022.7⟩ Accès au texte intégral et bibtex titre Semantics in Skel and Necro auteur Louis Noizet, Alan Schmitt article ICTCS 2022 – Italian Conference on Theoretical Computer Science , Sep 2022, Rome, Italy. pp.1-17Accès au texte intégral et bibtex titre End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers auteur Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli article CAV 2022 – 34th International Conference on Computer Aided Verification , Aug 2022, Haifa, Israel. pp.1-23Accès au texte intégral et bibtex titre Constant Time Secure Embedded Systems Through Hardware/Software Cooperation auteur Jean-Loup Hatchikian-Houdot article RESSI 2022 – Rendez-vous de la Recherche et de l’Enseignement de la Sécurité des Systèmes d’Information , May 2022, Chambon-sur-Lac, France. pp.1-3Accès au texte intégral et bibtex titre Certified Abstract Machines for Skeletal Semantics auteur Guillaume Ambal, Sergueï Lenglet, Alan Schmitt article CPP 2022 – 11th ACM SIGPLAN International Conference on Certified Programs and Proofs , Jan 2022, Philadelphia, United States. pp.1-13, ⟨10.1145/3497775.3503676⟩ Accès au texte intégral et bibtex Reports
titre Updated SPARTA SRIA (Roadmap v3) auteur Thomas Jensen article INRIA. 2022, pp.1-117 Accès au texte intégral et bibtex Theses
titre Formal Verification of Just-in-Time Compilation auteur Aurèle Barriere article Other [cs.OH]. École normale supérieure de Rennes, 2022. English. ⟨NNT : 2022ENSR0038⟩ Accès au texte intégral et bibtex titre A Meta-Approach to Describe Effectful and Distributed Semantics auteur Adam Khayam article Computer Vision and Pattern Recognition [cs.CV]. Université Rennes 1, 2022. English. ⟨NNT : 2022REN1S070⟩ Accès au texte intégral et bibtex titre Contrôle vérifié de flux d’information appliqué aux systèmes cyber-physiques auteur Jean-Joseph Marty article Systèmes embarqués. Université de Rennes, 2022. Français. ⟨NNT : 2022REN1S086⟩ Accès au texte intégral et bibtex titre Skeletal semantics transformations auteur Guillaume Ambal article Programming Languages [cs.PL]. Université Rennes 1, 2022. English. ⟨NNT : 2022REN1S057⟩ Accès au texte intégral et bibtex
