Publications HAL de la structure epicure 2024
Conference papers
titre Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation auteur Pierre Lermusiaux, Benoît Montagu article ESOP 2024 – 33rd European Symposium on Programming , Apr 2024, Luxembourg, Luxembourg. pp.391-420, ⟨10.1007/978-3-031-57267-8_15⟩ Accès au texte intégral et bibtex titre From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert auteur Sandrine Blazy article FASE 2024 – 27th International Conference on Fundamental Approaches to Software Engineering , Apr 2024, Luxembourg, Luxembourg. pp.1-21, ⟨10.1007/978-3-031-57259-3_1⟩ Accès au texte intégral et bibtex titre Skeletal Semantics of a Fragment of Python auteur Martin Andrieux, Alan Schmitt article 35es Journées Francophones des Langages Applicatifs (JFLA 2024) , Jan 2024, Saint-Jacut-de-la-Mer, FranceAccès au texte intégral et bibtex Proceedings
titre JFLA 2024 – 35es Journées Francophones des Langages Applicatifs auteur Delphine Demange, Adrien Guatto article 35es Journées Francophones des Langages Applicatifs (JFLA 2024) , pp.1-328, 2024Accès au texte intégral et bibtex Reports
titre Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation (Extended Version) auteur Pierre Lermusiaux, Benoît Montagu article RR-9536, Inria. 2024, pp.38 Accès au texte intégral et bibtex titre Réduire les émissions GES de nos déplacements professionnels : Une Démarche collaborative à l’IRISA/Inria auteur Elise Bannier, Simon Castellan, Steven Derrien, Francesca Galassi, Laurent Garnier, Ludovic Hoyet, Antoine l’Azou, Noé Lahaye, Marc J.-M. Macé, Olivier Martineau, Arthur Masson, Thomas Maugey, Benjamin Ninassi, Erven Rohou, Matthieu Simonin, François Taïani article Groupe de travail « missions » IRISA / Centre Inria de l’Université de Rennes. 2024, pp.1-16 Accès au texte intégral et bibtex Preprints, Working Papers, …
titre Leaf-First Zipper Semantics auteur Sergueï Lenglet, Alan Schmitt article 2024 Accès au texte intégral et bibtex 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, 7 (POPL), pp.249-277. ⟨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 Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification auteur Shenghao Yuan, Benjamin Lion, Frédéric Besson, Jean-Pierre Talpin article SETTA 2023 – 9th International Symposium Dependable Software Engineering. Theories, Tools, and Applications , Nov 2023, Nanjing (Chine), China. pp.385-401, ⟨10.1007/978-981-99-8664-4_22⟩ Accès au texte intégral et bibtex titre A Systematic Evaluation of Automated Tools for Side-Channel Vulnerabilities Detection in Cryptographic Libraries auteur Antoine Geimer, Mathéo Vergnolle, Frédéric Recoules, Lesly-Ann Daniel, Sébastien Bardin, Clémentine Maurice article CCS 2023 – ACM SIGSAC Conference on Computer and Communications Security , Nov 2023, Copenhagen, Denmark. pp.1690-1704, ⟨10.1145/3576915.3623112⟩ Accès au texte intégral et bibtex 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 Extracting ODRL Digital Right Representations from License Texts using AMR auteur Malo Revel, Aurélien Lamercerie, Annie Foret, Zoltan Miklos article ASAIL 2023 – Automated Semantic Analysis of Information in Legal Text , Sep 2023, Braga, Portugal. pp.1-7Accè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 2023 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW) , Jul 2023, Delft, Netherlands. pp.1-7Accè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. pp.1-15, ⟨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 JFLA 2023 – 34èmes Journées Francophones des Langages Applicatifs , pp.1-308, 2023, Journées Francophones des Langages ApplicatifsAccè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 , LIMITS, pp.1-11, 2023, ⟨10.21428/bf6fb269.265c52ce⟩ 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 Theses
titre Static Analysis of Algebraic Data Types and Arrays auteur Santiago Bautista article Computer Science [cs]. ENS Rennes, 2023. English. ⟨NNT : ⟩ Accès au bibtex titre Secure compilation against side channel attacks auteur Gautier Raimondi article Cryptography and Security [cs.CR]. Université de Rennes, 2023. English. ⟨NNT : 2023URENS094⟩ 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 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 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 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
