Publications HAL de la structure epicure 2025
Conference papers
titre A Mechanized Semantics for Dataflow Circuits auteur Tony Law, Delphine Demange, Sandrine Blazy article ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity , Oct 2025, Singapore, SingaporeAccès au bibtex titre Formal Verification of WTO-based Dataflow Solvers auteur Roméo La Spina, Delphine Demange, Sandrine Blazy article 34th European Symposium on Programming , May 2025, Hamilton, CanadaAccès au bibtex 2024
Journal articles
titre The Salto Project: Static Analysis of OCaml Programs by Abstract Interpretation auteur Pierre Lermusiaux, Benoît Montagu article ERCIM News , 2024, Special theme: Software Security, October 2024 (139), pp.24Accès au texte intégral et bibtex titre Axiomatising an information flow logic based on partial equivalence relations auteur Andrzej Filinski, Ken Friis Larsen, Thomas Jensen article International Journal on Software Tools for Technology Transfer , 2024, 26 (4), pp.445-461. ⟨10.1007/s10009-024-00756-z⟩ Accès au bibtex titre An input–output relational domain for algebraic data types and functional arrays auteur Santiago Bautista, Thomas Jensen, Benoît Montagu article Formal Methods in System Design , 2024, ⟨10.1007/s10703-024-00456-z⟩ Accès au texte intégral et bibtex titre Design and Implementation of Static Analyses for Tezos Smart Contracts auteur Luca Olivieri, Luca Negrini, Vincenzo Arceri, Thomas Jensen, Fausto Spoto article Distributed Ledger Technologies: Research and Practice , 2024, pp.1-23. ⟨10.1145/3643567⟩ Accès au bibtex Conference papers
titre Verification of programs with ADTs using Shallow Horn Clauses auteur Théo Losekoot, Thomas Genet, Thomas Jensen article Static Analysis Symposium , Roberto Giacobazzi, Alessandra Gorla, Oct 2024, Pasadena (CA), United StatesAccès au texte intégral et bibtex titre Formal Hardware/Software Models for Cache Locking Enabling Fast and Secure Code auteur Hatchikian-Houdot Jean-Loup, Pierre Wilke, Frédéric Besson, Guillaume Hiet article ESORICS 2024 – 29th European Symposium on Research in Computer Security , Tomasz Marciniak; Michał Choraś; Sokratis Katsikas; Joaquin Garcia-Alfaro; Rafał Kozik, Sep 2024, Bydgoszcz, Poland. pp.153-173, ⟨10.1007/978-3-031-70896-1_8⟩ Accès au texte intégral et bibtex titre End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT auteur Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin article CAV 2024 – 36th International Conference on Computer Aided Verification , Jul 2024, Montreal, Canada. pp.325-347, ⟨10.1007/978-3-031-65627-9_16⟩ Accès au texte intégral et bibtex titre Optimizing a Non-Deterministic Abstract Machine with Environments auteur Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt article FSCD 2024 – 9th International Conference on Formal Structures for Computation and Deduction , Jul 2024, Tallinn, Estonia. pp.1-22, ⟨10.4230/LIPIcs.FSCD.2024.11⟩ Accès au texte intégral et bibtex titre Leaf-First Zipper Semantics auteur Sergueï Lenglet, Alan Schmitt article FORTE 2024 – 44th International Conference on Formal Techniques for Distributed Objects, Components, and Systems , Jun 2024, Groningen, Netherlands. ⟨10.1007/978-3-031-62645-6_7⟩ Accès au texte intégral et bibtex 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 Reducing GHG emissions from business travel: A collaborative approach at 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 Theses
titre Analyses statiques pour sémantiques squelettiques auteur Vincent Rébiscoul article Programming Languages [cs.PL]. Université de Rennes, 2024. English. ⟨NNT : 2024URENS040⟩ Accès au texte intégral et bibtex Preprints, Working Papers, …
titre Optimizing a Non-Deterministic Abstract Machine with Environments auteur Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt article 2024 Accès au texte intégral et bibtex titre Leaf-First Zipper Semantics auteur Sergueï Lenglet, Alan Schmitt article 2024 Accès au texte intégral et bibtex titre Verification of programs with ADTs using Shallow Horn Clauses — extended version auteur Théo Losekoot, Thomas Genet, Thomas Jensen article 2024 Accès au texte intégral et bibtex titre Disentangling Parallelism and Interference in Game Semantics auteur Simon Castellan, Pierre Clairambault 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. Université de Rennes, 2023. English. ⟨NNT : 2023URENE010⟩ Accès au texte intégral et 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 titre On the mechanized verification of the meta-theory of contracts and its instantiation to differential dynamic logic auteur Stéphane Kastenbaum article Other [cs.OH]. Université de Rennes, 2023. English. ⟨NNT : 2023URENS013⟩ 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 Verified information flow control applied to cyber-physical systems 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
