Publications

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-70

Accès au texte intégral et bibtex

2022

Conference papers

titre

Semantic foundations for cost analysis of pipeline-optimized programs

auteur

Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe

article

SAS 2022 – 29th International Symposium on Static Analysis, Dec 2022, Auckland, New Zealand. ⟨10.1007/978-3-031-22308-2_17⟩

Accè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

titre

A Flow-Insensitive-Complete Program Representation

auteur

Solène Mirliaz, David Pichardie

article

23rd International Conference Verification, Model Checking, and Abstract Interpretation (VMCAI 2022 ), Jan 2022, Philadelphia, United States. ⟨10.1007/978-3-030-94583-1_10⟩

Accès au texte intégral et bibtex

Books

titre

33èmes journées francophones des langages applicatifs

auteur

Chantal Keller, Timothy Bourke, Sandrine Blazy, Frédéric Bour, Guillaume Bury, Stefania Dumbrava, Diane Gallois-Wong, Adrien Guatto, David Janin, Marie Kerjean, Luc Pellissier, Mário Pereira, Alix Trieu, Yannick Zakowski

article

Chantal Keller; Timothy Bourke. , pp.1-292, 2022

Accès au texte intégral et bibtex

Reports

titre

Non-Deterministic Abstract Machines

auteur

Małgorzata Biernacka, Dariusz Biernacki, Serguei Lenglet, Alan Schmitt

article

[Research Report] RR-9475, Inria. 2022, pp.1-33

Accès au texte intégral et bibtex

titre

A Formal Model of Interrupt-based Checkpointing with Peripherals

auteur

Pierre-Evariste Dagand, Gautier Berthou, Delphine Demange, Tanguy Risset

article

[Research Report] IRIF; IRISA; INSA RENNES. 2022, pp.1-36

Accès au texte intégral et bibtex

titre

Stating and Handling Semantics with Skel and Necro

auteur

Louis Noizet, Alan Schmitt

article

[Research Report] RR-9449, Inria Rennes – Bretagne Atlantique. 2022, pp.1-23

Accès au texte intégral et bibtex

2021

Journal articles

titre

Verification of Program Transformations with Inductive Refinement Types

auteur

Ahmad Salim Al-Sibahi, Thomas P Jensen, Aleksandar S Dimovski, Andrzej Wąsowski

article

ACM Transactions on Software Engineering and Methodology, 2021, 30 (1), pp.1-33. ⟨10.1145/3409805⟩

Accès au texte intégral et bibtex

titre

Formally verified speculation and deoptimization in a JIT compiler

auteur

Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek

article

Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.26. ⟨10.1145/3434327⟩

Accès au texte intégral et bibtex

Conference papers

titre

Verified Functional Programming of an Abstract Interpreter

auteur

Lucas Franceschino, Jean-Pierre Talpin, David Pichardie

article

SAS 2021 – 28th Static Analysis Symposium, Oct 2021, Chicago, United States. pp.1-20

Accès au texte intégral et bibtex

titre

Itauto: An Extensible Intuitionistic SAT Solver

auteur

Frédéric Besson

article

ITP 2021 – 12th International Conference on Interactive Theorem Proving, Jun 2021, Roma, Italy. pp.1-18, ⟨10.4230/LIPIcs.ITP.2021.9⟩

Accès au texte intégral et bibtex

titre

Secure Compilation of Constant-Resource Programs

auteur

Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie

article

CSF 2021 – 34th IEEE Computer Security Foundations Symposium, Jun 2021, Dubrovnik, Croatia. pp.1-12

Accès au texte intégral et bibtex

titre

Trace-Based Control-Flow Analysis

auteur

Benoît Montagu, Thomas Jensen

article

PLDI 2021 – 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Jun 2021, Virtual, Canada. pp.1-15, ⟨10.1145/3453483.3454057⟩

Accès au texte intégral et bibtex

titre

JSkel: Towards a Formalization of JavaScript’s Semantics

auteur

Adam Khayam, Louis Noizet, Alan Schmitt

article

JFLA 2021 – Journées Francophones des Langages Applicatifs, Apr 2021, Virtuelles, France. pp.1-22

Accès au texte intégral et bibtex

Book sections

titre

Categories with Families: Unityped, Simply Typed, and Dependently Typed

auteur

Pierre Clairambault, Simon Castellan, Peter Dybjer

article

Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, 20, Springer International Publishing, pp.135-180, 2021, Outstanding Contributions to Logic, ⟨10.1007/978-3-030-66545-6_5⟩

Accès au bibtex

Proceedings

titre

CC 2021: Proceedings of the 30th ACM SIGPLAN International Conference on Compiler Construction

auteur

Aaron Smith, Delphine Demange, Rajiv Gupta

article

CC ’21 – 30th ACM SIGPLAN International Conference on Compiler Construction, Virtual Republic of Korea, ACM, 2021, ⟨10.1145/3446804⟩

Accès au bibtex

Theses

titre

Verified Secure Compilation against Timing Side-Channels

auteur

Rémi Hutin

article

Cryptographie et sécurité [cs.CR]. École normale supérieure de Rennes, 2021. Français. ⟨NNT : 2021ENSR0029⟩

Accès au texte intégral et bibtex

Preprints, Working Papers, …

titre

A Flow-Insensitive-Complete Program Representation

auteur

Solène Mirliaz, David Pichardie

article

2021

Accès au texte intégral et bibtex

titre

The Mays and Musts of Concurrent Strategies

auteur

Simon Castellan, Pierre Clairambault, Glynn Winskel

article

2021

Accès au texte intégral et bibtex

2020

Journal articles

titre

Stable relations and abstract interpretation of higher-order programs

auteur

Benoît Montagu, Thomas Jensen

article

Proceedings of the ACM on Programming Languages, 2020, 4 (ICFP), pp.1-30. ⟨10.1145/3409001⟩

Accès au texte intégral et bibtex

titre

Formal verification of a constant-time preserving C compiler

auteur

Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu

article

Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩

Accès au texte intégral et bibtex

titre

HOπ in Coq

auteur

Guillaume Ambal, Sergueï Lenglet, Alan Schmitt

article

Journal of Automated Reasoning, 2020, ⟨10.1007/s10817-020-09553-0⟩

Accès au texte intégral et bibtex

titre

Regular Language Type Inference with Term Rewriting – extended version

auteur

Timothée Haudebourg, Thomas Genet, Thomas Jensen

article

Proceedings of the ACM on Programming Languages, 2020, International Conference on Functional Programming (ICFP), 4 (ICFP), pp.1-29. ⟨10.1145/3408994⟩

Accès au texte intégral et bibtex

Conference papers

titre

Numeric Domains Meet Algebraic Data Types

auteur

Santiago Bautista, Thomas Jensen, Benoît Montagu

article

NSAD 2020 – 9th International Workshop on Numerical and Symbolic Abstract Domains, Nov 2020, Virtual, United States. pp.12-16, ⟨10.1145/3427762.3430178⟩

Accès au texte intégral et bibtex

titre

Termination of Ethereum’s Smart Contracts

auteur

Thomas Genet, Thomas Jensen, Justine Sauvage

article

SECRYPT 2020 – 17th International Conference on Security and Cryptography, Jul 2020, Lieusaint – Paris / Virtual, France. pp.39-51, ⟨10.5220/0009564100390051⟩

Accès au texte intégral et bibtex

titre

A Fast Verified Liveness Analysis in SSA Form

auteur

Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie

article

IJCAR 2020- International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.324-340, ⟨10.1007/978-3-030-51054-1_19⟩

Accès au texte intégral et bibtex

titre

Intermittent Computing with Peripherals, Formally Verified

auteur

Gautier Berthou, Pierre-Evariste Dagand, Delphine Demange, Rémi Oudin, Tanguy Risset

article

LCTES ’20 – 21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, Jun 2020, London / Virtual, United Kingdom. pp.85-96, ⟨10.1145/3372799.3394365⟩

Accès au texte intégral et bibtex

titre

Formalisation de Sémantiques Squelettiques

auteur

Louis Noizet, Alan Schmitt

article

JLFA 2020 – Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. pp.1-14

Accès au texte intégral et bibtex

Reports

titre

Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step

auteur

Guillaume Ambal, Alan Schmitt, Sergueï Lenglet

article

[Research Report] RR-9363, Inria Rennes – Bretagne Atlantique. 2020

Accès au texte intégral et bibtex

titre

Termination of Ethereum’s Smart Contracts

auteur

Thomas Genet, Thomas Jensen, Justine Sauvage

article

[Research Report] Univ Rennes, Inria, CNRS, IRISA. 2020

Accès au texte intégral et bibtex

titre

Concurrent Game Semantics: Easy as Pi

auteur

Simon Castellan, Léo Stefanesco, Nobuko Yoshida

article

[Research Report] Inria. 2020

Accès au texte intégral et bibtex

Theses

titre

Automatic verification of higher-order functional programs using regular tree languages

auteur

Timothée Haudebourg

article

Programming Languages [cs.PL]. Université Rennes 1, 2020. English. ⟨NNT : 2020REN1S060⟩

Accès au texte intégral et bibtex

2019

Journal articles

titre

CompCertS: A Memory-Aware Verified C Compiler using a Pointer as Integer Semantics

auteur

Frédéric Besson, Sandrine Blazy, Pierre Wilke

article

Journal of Automated Reasoning, 2019, 63 (2), pp.369-392. ⟨10.1007/s10817-018-9496-y⟩

Accès au texte intégral et bibtex

titre

A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data

auteur

Frédéric Besson, Sandrine Blazy, Pierre Wilke

article

Journal of Automated Reasoning, 2019, 62 (4), pp.433-480. ⟨10.1007/s10817-017-9439-z⟩

Accès au texte intégral et bibtex

titre

Inferring frame conditions with static correlation analysis

auteur

Oana Andreescu, Thomas Jensen, Stéphane Lescuyer, Benoît Montagu

article

Proceedings of the ACM on Programming Languages, 2019, 3 (POPL), pp.1-29. ⟨10.1145/3290360⟩

Accès au bibtex

titre

Verifying constant-time implementations by abstract interpretation

auteur

Sandrine Blazy, David Pichardie, Alix Trieu

article

Journal of Computer Security, 2019, 27 (1), pp.137–163. ⟨10.3233/JCS-181136⟩

Accès au texte intégral et bibtex

titre

Skeletal Semantics and their Interpretations

auteur

Martin Bodin, Philippa Gardner, Thomas Jensen, Alan Schmitt

article

Proceedings of the ACM on Programming Languages, In press, 44, pp.1-31. ⟨10.1145/3290357⟩

Accès au texte intégral et bibtex

Conference papers

titre

Teaching Deductive Verification in Why3 to Undergraduate Students

auteur

Sandrine Blazy

article

FM Tea (Formal Methods Teaching), Oct 2019, Porto, Portugal. pp.52-66, ⟨10.1007/978-3-030-32441-4_4⟩

Accès au bibtex

titre

Information-Flow Preservation in Compiler Optimisations

auteur

Frédéric Besson, Alexandre Dang, Thomas Jensen

article

CSF 2019 – 32nd IEEE Computer Security Foundations Symposium, Jun 2019, Hoboken, United States. pp.1-13

Accès au texte intégral et bibtex

titre

Octogones entiers pour le problème RCPSP

auteur

Pierre Talbot, David Cachera, Eric Monfroy, Charlotte Truchet

article

JFPC 2019 – Journées Francophones de Programmation par Contraintes, Jun 2019, Albi, France. pp.1-10

Accès au texte intégral et bibtex

titre

Compiling Sandboxes: Formally Verified Software Fault Isolation

auteur

Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, Pierre Wilke

article

ESOP 2019 – 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.499-524, ⟨10.1007/978-3-030-17184-1_18⟩

Accès au texte intégral et bibtex

titre

Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions

auteur

Sandrine Blazy, Rémi Hutin

article

CPP 2019 – 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Cascais, Portugal. pp.196-208, ⟨10.1145/3293880.3294103⟩

Accès au texte intégral et bibtex

Reports

titre

Flow insensitive relational static analysis

auteur

Solène Mirliaz, David Pichardie

article

[Internship report] ENS Rennes; Université Rennes 1. 2019

Accès au texte intégral et bibtex

Theses

titre

Verifying Software Fault Isolation

auteur

Julien Lepiller

article

Performance [cs.PF]. Université de Rennes, 2019. English. ⟨NNT : 2019REN1S067⟩

Accès au texte intégral et bibtex

titre

Secure compilation for memory protection

auteur

Alexandre Dang

article

Cryptography and Security [cs.CR]. Université de Rennes, 2019. English. ⟨NNT : 2019REN1S111⟩

Accès au texte intégral et bibtex

2018

Journal articles

titre

Graph Queries: From Theory to Practice

auteur

Angela Bonifati, Stefania Dumbrava

article

SIGMOD record, 2018, 47 (4), pp.5-16. ⟨10.1145/3335409.3335411⟩

Accès au texte intégral et bibtex

titre

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

auteur

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

article

Journal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9489-x⟩

Accès au texte intégral et bibtex

Conference papers

titre

Verification of High-Level Transformations with Inductive Refinement Types

auteur

Ahmad Salim Al-Sibahi, Aleksandar S. Dimovski, Thomas Jensen, Andrzej Wasowski

article

GPCE 2018 – 17th International Conference on Generative Programming: Concepts & Experience, Nov 2018, Boston, United States. pp.147-160, ⟨10.1145/3278122.3278125⟩

Accès au texte intégral et bibtex

titre

Securing Compilation Against Memory Probing

auteur

Frédéric Besson, Alexandre Dang, Thomas Jensen

article

PLAS ’18 – 13th Workshop on Programming Languages and Analysis for Security, Oct 2018, Toronto, Canada. pp.29-40, ⟨10.1145/3264820.3264822⟩

Accès au texte intégral et bibtex

titre

MLExplain

auteur

Kévin Le Bon, Alan Schmitt

article

OCaml 2018, Sep 2018, Saint Louis, United States. pp.1-4

Accès au texte intégral et bibtex

titre

Modular Software Fault Isolation as Abstract Interpretation

auteur

Frédéric Besson, Thomas Jensen, Julien Lepiller

article

SAS 2018 – 25th International Static Analysis Symposium, Aug 2018, Freiburg, Germany. pp.166-186, ⟨10.1007/978-3-319-99725-4_12⟩

Accès au texte intégral et bibtex

titre

Completeness of Tree Automata Completion

auteur

Thomas Genet

article

FSCD 2018 – 3rd International Conference on Formal Structures for Computation and Deduction, Jul 2018, Oxford, United Kingdom. pp.1-20, ⟨10.4230/LIPIcs.FSCD.2018.15⟩

Accès au texte intégral et bibtex

titre

Vérifier des fonctions d’ordre supérieur à l’aide d’automates d’arbre

auteur

Thomas Genet, Timothée Haudebourg, Thomas Jensen

article

17èmes Journées AFADL 2018 – Approches Formelles dans l’Assistance au Développement de Logiciels, May 2018, Grenoble, France. pp.1-3

Accès au texte intégral et bibtex

titre

JSExplain: A Double Debugger for JavaScript

auteur

Arthur Charguéraud, Alan Schmitt, Thomas Wood

article

The Web Conference 2018, Apr 2018, Lyon, France. pp.1-9, ⟨10.1145/3184558.3185969⟩

Accès au texte intégral et bibtex

titre

Automata and Equations based Approximations for Reachability Analysis

auteur

Thomas Genet

article

WRLA 2018 – 12th International Workshop on Rewriting Logic and its Applications, Apr 2018, Thessalonique, Greece. pp.1

Accès au bibtex

titre

Verifying Higher-Order Functions with Tree Automata

auteur

Thomas Genet, Timothée Haudebourg, Thomas Jensen

article

FoSSaCS 2018 – 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.565-582, ⟨10.1007/978-3-319-89366-2_31⟩

Accès au texte intégral et bibtex

titre

Extending Timbuk to Verify Functional Programs

auteur

Thomas Genet, Tristan Gillard, Timothée Haudebourg, Sébastien Lê Cong

article

WRLA 2018 – 12th International Worshop on Rewriting Logic and its Applications, Apr 2018, Thessalonique, Greece. pp.153-163, ⟨10.1007/978-3-319-99840-4_9⟩

Accès au texte intégral et bibtex

titre

Verified Compilation of Linearizable Data Structures: Mechanizing Rely Guarantee for Semantic Refinement

auteur

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie

article

SAC 2018 – The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France. pp.1881-1890, ⟨10.1145/3167132.3167333⟩

Accès au texte intégral et bibtex

titre

Semantic reasoning about the sea of nodes

auteur

Delphine Demange, Yon Fernández de Retana, David Pichardie

article

CC 2018 – 27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. pp.163-173, ⟨10.1145/3178372.3179503⟩

Accès au texte intégral et bibtex

titre

CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler

auteur

Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, Sandrine Blazy

article

ERTS2 2018 – 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9

Accès au texte intégral et bibtex

titre

HOπ in Coq

auteur

Sergueï Lenglet, Alan Schmitt

article

CPP 2018 – The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.14, ⟨10.1145/3167083⟩

Accès au texte intégral et bibtex

Theses

titre

Non local analyses certification with an annotated semantics

auteur

Gurvan Cabon

article

Software Engineering [cs.SE]. Université de Rennes, 2018. English. ⟨NNT : 2018REN1S078⟩

Accès au texte intégral et bibtex

titre

Verifying constant-time implementations in a verified compilation toolchain

auteur

Alix Trieu

article

Cryptography and Security [cs.CR]. Université de Rennes, 2018. English. ⟨NNT : 2018REN1S099⟩

Accès au texte intégral et bibtex

2017

Journal articles

titre

Reachability Analysis of Innermost Rewriting – extended version

auteur

Thomas Genet, Yann Salmon

article

Logical Methods in Computer Science, 2017, ⟨10.2168/LMCS-???⟩

Accès au texte intégral et bibtex

Conference papers

titre

Annotated multisemantics to prove Non-Interference analyses

auteur

Gurvan Cabon, Alan Schmitt

article

PLAS 2017 – ACM SIGSAC Workshop on Programming Languages and Analysis for Security, Oct 2017, Dallas, United States. ⟨10.1145/3139337.3139344⟩

Accès au texte intégral et bibtex

titre

GPFinder: Tracking the Invisible in Android Malware

auteur

Mourad Leslous, Valérie Viet Triem Tong, Jean-François Lalande, Thomas Genet

article

12th International Conference on Malicious and Unwanted Software, Oct 2017, Fajardo, Puerto Rico. pp.39-46, ⟨10.1109/MALWARE.2017.8323955⟩

Accès au texte intégral et bibtex

titre

Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology

auteur

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

article

ITP 2017 – 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. pp.496-513, ⟨10.1007/978-3-319-66107-0_31⟩

Accès au texte intégral et bibtex

titre

CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics

auteur

Frédéric Besson, Sandrine Blazy, Pierre Wilke

article

ITP 2017 – 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.81-97, ⟨10.1007/978-3-319-66107-0_6⟩

Accès au texte intégral et bibtex

titre

Hybrid information flow analysis against web tracking (invited talk)

auteur

Thomas Jensen

article

CRiSIS 2017 – 12th International Conference on Risks and Security of Internet and Systems, Sep 2017, Dinard, France. pp.1-33

Accès au texte intégral et bibtex

titre

Verifying Constant-Time Implementations by Abstract Interpretation

auteur

Sandrine Blazy, David Pichardie, Alix Trieu

article

European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway

Accès au texte intégral et bibtex

titre

Verified Translation Validation of Static Analyses

auteur

Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu

article

Computer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States

Accès au texte intégral et bibtex

titre

Formal methods for software security (invited talk)

auteur

Thomas Jensen

article

Journées Nationales 2017 Pré-GDR Sécurité Informatique, Jun 2017, Paris, France. pp.1-31

Accès au texte intégral et bibtex

titre

Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines

auteur

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt

article

LICS 2017 – 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005118⟩

Accès au texte intégral et bibtex

titre

Confusion de Type en C++: État de l’Art et Difficultés de Détection

auteur

Florent Saudel, Sandrine Blazy, Frédéric Besson

article

RESSI 2017 – Rendez-vous de la Recherche et de l’Enseignement de la Sécurité des Systèmes d’Information , May 2017, Grenoble/Autrans, France. pp.1-5

Accès au texte intégral et bibtex

titre

Closing the Gap – The Formally Verified Optimizing Compiler CompCert

auteur

Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, Christian Ferdinand

article

SSS’17: Safety-critical Systems Symposium 2017, Feb 2017, Bristol, United Kingdom. pp.163-180

Accès au texte intégral et bibtex

titre

Formal methods for software security (invited talk)

auteur

Thomas Jensen

article

FMF 2017 – Forum “Méthodes Formelles”, Jan 2017, Toulouse, France. pp.1-61

Accès au texte intégral et bibtex

titre

Structuring abstract interpreters through state and value abstractions

auteur

Sandrine Blazy, David Bühler, Boris Yakobowski

article

18th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI 2017), Jan 2017, Paris, France. pp.112-130, ⟨10.1007/978-3-319-52234-0_7⟩

Accès au bibtex

titre

Non-Interference through Annotated Multisemantics

auteur

Gurvan Cabon, Alan Schmitt

article

28ièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France

Accès au texte intégral et bibtex

Other publications

titre

SPAN+AVISPA for Verifying Cryptographic Protocols

auteur

Thomas Genet

article

2017

Accès au bibtex

Reports

titre

Verifying Higher-Order Functions with Tree Automata: Extended Version

auteur

Thomas Genet, Timothée Haudebourg, Thomas Jensen

article

[Technical Report] Irisa. 2017, pp.1-20

Accès au texte intégral et bibtex

titre

Compilation of Linearizable Data Structures

auteur

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie

article

[Research Report] ENS Rennes; IRISA, Inria Rennes; Université Rennes 1. 2017

Accès au texte intégral et bibtex

titre

Automata Completion and Regularity Preservation

auteur

Thomas Genet

article

[Research Report] IRISA, Inria Rennes. 2017

Accès au texte intégral et bibtex

titre

Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines

auteur

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt

article

[Research Report] RR-9052, Inria. 2017

Accès au texte intégral et bibtex

titre

A Short Isabelle Tutorial for the Functional Programmer

auteur

Thomas Genet, Jørgen Villadsen

article

[Research Report] IRISA. 2017, pp.1-5

Accès au texte intégral et bibtex

Theses

titre

Verification of a Concurrent Garbage Collector

auteur

Yannick Zakowski

article

Data Structures and Algorithms [cs.DS]. École normale supérieure de Rennes, 2017. English. ⟨NNT : 2017ENSR0010⟩

Accès au texte intégral et bibtex

titre

Static analysis of functional programs with an application to the frame problem in deductive verification

auteur

Oana Fabiana Andreescu

article

Other [cs.OH]. Université de Rennes, 2017. English. ⟨NNT : 2017REN1S047⟩

Accès au texte intégral et bibtex

titre

Formal models and verification of memory management in a hypervisor

auteur

Pauline Bolignano

article

Cryptography and Security [cs.CR]. Université de Rennes; Prove & Run, 2017. English. ⟨NNT : 2017REN1S026⟩

Accès au texte intégral et bibtex

titre

Structuring an Abstract Interpreter through Value and State Abstractions: EVA, an Evolved Value Analysis for Frama-C

auteur

David Bühler

article

Programming Languages [cs.PL]. Université de Rennes 1, 2017. English. ⟨NNT : ⟩

Accès au texte intégral et bibtex

2016

Journal articles

titre

A Verified Information-Flow Architecture

auteur

Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach

article

Journal of Computer Security, 2016, 24 (6), pp.689–734. ⟨10.3233/JCS-15784⟩

Accès au bibtex

titre

Improving static analyses of C programs with conditional predicates

auteur

Sandrine Blazy, David Bühler, Boris Yakobowski

article

Science of Computer Programming, 2016, 118, ⟨10.1145/2854065.2854082⟩

Accès au texte intégral et bibtex

titre

Termination criteria for tree automata completion

auteur

Thomas Genet

article

Journal of Logical and Algebraic Methods in Programming, 2016, 85, Issue 1, part 1, pp.3-33. ⟨10.1016/j.jlamp.2015.05.003⟩

Accès au texte intégral et bibtex

titre

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code

auteur

Sandrine Blazy, Vincent Laporte, David Pichardie

article

Journal of Automated Reasoning, 2016, 56 (3), pp.26. ⟨10.1007/s10817-015-9359-8⟩

Accès au texte intégral et bibtex

Conference papers

titre

An Abstract Memory Functor for Verified C Static Analyzers

auteur

Sandrine Blazy, Vincent Laporte, David Pichardie

article

ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. pp.14, ⟨10.1145/2951913.2951937⟩

Accès au texte intégral et bibtex

titre

Correlating Structured Inputs and Outputs in Functional Specifications

auteur

Oana Andreescu, Thomas Jensen, Stéphane Lescuyer

article

Software Engineering and Formal Methods, Jul 2016, Vienna, Austria. pp.19, ⟨10.1007/978-3-319-41591-8_7⟩

Accès au bibtex

titre

An Extended Buffered Memory Model With Full Reorderings

auteur

Gurvan Cabon, David Cachera, David Pichardie

article

FtFjp – Ecoop workshop, Jul 2016, Rome, Italy. pp.1 – 6, ⟨10.1145/2955811.2955816⟩

Accès au texte intégral et bibtex

titre

A Certified Compiler for Verifiable Computing

auteur

Cédric Fournet, Chantal Keller, Vincent Laporte

article

IEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal

Accès au texte intégral et bibtex

titre

Modeling and Abstraction of Memory Management in a Hypervisor

auteur

Pauline Bolignano, Thomas Jensen, Vincent Siles

article

Fundamental Approaches to Software Engineering (FASE’16), Apr 2016, Eindhoven, Netherlands. pp.214 – 230, ⟨10.1007/978-3-662-49665-7_13⟩

Accès au texte intégral et bibtex

titre

Mechanizing conventional SSA for a verified destruction with coalescing

auteur

Delphine Demange, Yon Fernandez de Retana

article

25th International Conference on Compiler Construction, Mar 2016, Barcelona, Spain

Accès au texte intégral et bibtex

titre

An Abstract Separation Logic for Interlinked Extensible Records

auteur

Martin Bodin, Thomas Jensen, Alan Schmitt

article

Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint-Malo, France

Accès au texte intégral et bibtex

titre

CompCert – A Formally Verified Optimizing Compiler

auteur

Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, Christian Ferdinand

article

ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Jan 2016, Toulouse, France

Accès au texte intégral et bibtex

titre

Formal Verification of Control-flow Graph Flattening

auteur

Sandrine Blazy, Alix Trieu

article

Certified Proofs and Programs (CPP 2016), Jan 2016, Saint-Petersburg, United States. pp.12, ⟨10.1145/2854065.2854082⟩

Accès au texte intégral et bibtex

titre

Hybrid Monitoring of Attacker Knowledge

auteur

Frédéric Besson, Nataliia Bielova, Thomas Jensen

article

29th IEEE Computer Security Foundations Symposium, 2016, Lisboa, Portugal

Accès au texte intégral et bibtex

Other publications

titre

Using JavaScript Monitoring to Prevent Device Fingerprinting

auteur

Nataliia Bielova, Frédéric Besson, Thomas Jensen

article

2016

Accès au texte intégral et bibtex

Proceedings

titre

Verified Software: Theories, Tools, and Experiments – 8th International Conference, VSTTE 2016, Toronto, Canada, July 17-18, 2016. Proceedings

auteur

Sandrine Blazy, Marsha Chechik

article

Sandrine Blazy and Marsha Chechik. Verified Software: Theories, Tools, and Experiments – 8th International Conference, VSTTE 2016, Jul 2016, Toronto, Canada. 9971, Springer, 2016, Lecture Notes in Computer Science

Accès au bibtex

Theses

titre

Certified semantics and analysis of JavaScript

auteur

Martin Bodin

article

Programming Languages [cs.PL]. Université de Rennes, 2016. English. ⟨NNT : 2016REN1S087⟩

Accès au texte intégral et bibtex

titre

Formally verified compilation of low-level C code

auteur

Pierre Wilke

article

Programming Languages [cs.PL]. Université de Rennes, 2016. English. ⟨NNT : 2016REN1S088⟩

Accès au texte intégral et bibtex

2015

Journal articles

titre

Efficiently Deciding µ-calculus with Converse over Finite Trees

auteur

Pierre Genevès, Nabil Layaïda, Alan Schmitt, Nils Gesbert

article

ACM Transactions on Computational Logic, 2015, 16 (2), pp.41. ⟨10.1145/2724712⟩

Accès au texte intégral et bibtex

Conference papers

titre

An ω-Algebra for Real-Time Energy Problems

auteur

David Cachera, Uli Fahrenberg, Axel Legay

article

35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2015, Bengaluru, India. pp.394

Accès au texte intégral et bibtex

titre

Dependency Analysis of Functional Specifications with Algebraic Data Structures

auteur

Oana Andreescu, Thomas Jensen, Stephane Lescuyer

article

17th International Conference on Formal Engineering Methods, ICFEM 2015, Michael Butler Sylvain Conchon Fatiha Zaïdi, Nov 2015, Paris, France. pp.18, ⟨10.1007/978-3-319-25423-4_8⟩

Accès au bibtex

titre

Data Tainting and Obfuscation: Improving Plausibility of Incorrect Taint

auteur

Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent

article

Source Code Analysis and Manipulation (SCAM), Sep 2015, Bremen, Germany

Accès au texte intégral et bibtex

titre

Howe’s Method for Contextual Semantics

auteur

Sergueï Lenglet, Alan Schmitt

article

CONCUR 2015 26th International Conference on Concurrency Theory, Sep 2015, Madrid, Spain. ⟨10.4230/LIPIcs.CONCUR.2015.212⟩

Accès au texte intégral et bibtex

titre

Hybrid Typing of Secure Information Flow in a JavaScript-like Language

auteur

José Fragoso Santos, Thomas Jensen, Tamara Rezk, Alan Schmitt

article

International Symposium on Trustworthy Global Computing, Aug 2015, Madrid, Spain

Accès au texte intégral et bibtex

titre

A Concrete Memory Model for CompCert

auteur

Frédéric Besson, Sandrine Blazy, Pierre Wilke

article

ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. pp.67-83, ⟨10.1007/978-3-319-22102-1_5⟩

Accès au texte intégral et bibtex

titre

Validating Dominator Trees for a Fast, Verified Dominance Test

auteur

Sandrine Blazy, Delphine Demange, David Pichardie

article

Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_6⟩

Accès au texte intégral et bibtex

titre

HOCore in Coq

auteur

Petar Maksimovic, Alan Schmitt

article

Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_19⟩

Accès au texte intégral et bibtex

titre

Expressive Logical Combinators for Free

auteur

Pierre Genevès, Alan Schmitt

article

International Joint Conference on Artificial Intelligence (IJCAI 2015), Jul 2015, Buenos Aires, Argentina

Accès au texte intégral et bibtex

titre

Attack Trees with Sequential Conjunction

auteur

Barbara Kordy, Ravi Jhawar, Sjouke Mauw, Sasa Radomirovic, Roland Trujillo-Rasua

article

30th IFIP International Information Security Conference (SEC), May 2015, Hamburg, Germany. pp.339-353, ⟨10.1007/978-3-319-18467-8_23⟩

Accès au texte intégral et bibtex

titre

Kharon : Découvrir, comprendre et reconnaître des malware Android par suivi de flux d’information

auteur

Radoniaina Andriatsimandefitra Ratsisahanana, Thomas Genet, Laurent Guillo, Jean-François Lalande, David Pichardie, Valérie Viet Triem Tong

article

Rendez-vous de la Recherche et de l’Enseignement de la Sécurité des Systèmes d’Information, May 2015, Troyes, France

Accès au texte intégral et bibtex

titre

A formally-verified C static analyzer

auteur

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie

article

POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩

Accès au texte intégral et bibtex

titre

Certified Abstract Interpretation with Pretty-Big-Step Semantics

auteur

Martin Bodin, Thomas Jensen, Alan Schmitt

article

Certified Programs and Proofs (CPP 2015), Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693174⟩

Accès au texte intégral et bibtex

titre

HOCore in Coq

auteur

Martín Escarrá, Petar Maksimović, Alan Schmitt

article

Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d’Ajol, France

Accès au texte intégral et bibtex

titre

Formal verification of compilers and static analyzers.

auteur

Sandrine Blazy

article

PLMW@POPL 2015 – Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India

Accès au bibtex

titre

Reachability Analysis of Innermost Rewriting

auteur

Thomas Genet, Yann Salmon

article

Rewriting Techniques and Applications 2015, 2015, Warshaw, Poland

Accès au texte intégral et bibtex

titre

Verified Validation of Program Slicing

auteur

Sandrine Blazy, Andre Maroneze, David Pichardie

article

CPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, ⟨10.1145/2676724.2693169⟩

Accès au bibtex

titre

Verifying a Real-Time Language with Constraints

auteur

Anicet Bart, Charlotte Truchet, Eric Monfroy

article

27th IEEE International Conference on Tools with Artificial Intelligence, 2015, Vietri sul Mare, Italy. ⟨10.1109/ICTAI.2015.124⟩

Accès au bibtex

titre

Verifying Fast and Sparse SSA-based Optimizations in Coq.

auteur

Delphine Demange, David Pichardie, Léo Stefanesco

article

24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom

Accès au bibtex

titre

Vers un outil de vérification formelle légere pour OCaml

auteur

Thomas Genet, Barbara Kordy, Amaury Vansyngel

article

AFADL, 2015, Bordeaux, France. pp.6

Accès au texte intégral et bibtex

Proceedings

titre

Static Analysis Symposium – 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015. Proceedings

auteur

Sandrine Blazy, Thomas Jensen

article

Sandrine Blazy; Thomas Jensen. Static Analysis Symposium – 22nd International Symposium, SAS 2015, Aug 2015, Saint-Malo, France. Lecture Notes in Computer Science (LNCS) (9291), Springer, pp.335, 2015, 978-3-662-48287-2

Accès au bibtex

Reports

titre

A Short SPAN+AVISPA Tutorial

auteur

Thomas Genet

article

[Research Report] IRISA. 2015

Accès au texte intégral et bibtex

titre

Howe’s Method for Contextual Semantics

auteur

Sergueï Lenglet, Alan Schmitt

article

[Research Report] RR-8750, Inria. 2015, pp.31

Accès au texte intégral et bibtex

Theses

titre

Reachability analysis for functional programs with innermost evaluation strategy

auteur

Yann Salmon

article

Performance et fiabilité [cs.PF]. Université Rennes 1, 2015. Français. ⟨NNT : 2015REN1S085⟩

Accès au texte intégral et bibtex

titre

Verified static analyzes for low-level languages

auteur

Vincent Laporte

article

Programming Languages [cs.PL]. Université de Rennes, 2015. English. ⟨NNT : 2015REN1S078⟩

Accès au texte intégral et bibtex

2014

Journal articles

titre

Atomicity Refinement for Verified Compilation

auteur

Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek

article

ACM Transactions on Programming Languages and Systems (TOPLAS), 2014, pp.30

Accès au bibtex

titre

Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases

auteur

David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner

article

Science of Computer Programming, 2014, 93, pp.21. ⟨10.1016/j.scico.2014.02.028⟩

Accès au bibtex

titre

Formal Verification of an SSA-based Middle-end for CompCert

auteur

Gilles Barthe, Delphine Demange, David Pichardie

article

ACM Transactions on Programming Languages and Systems (TOPLAS), 2014, 36 (1), pp.35. ⟨10.1145/2579080⟩

Accès au bibtex

Conference papers

titre

GLV/GLS Decomposition, Power Analysis, and Attacks on ECDSA Signatures with Single-Bit Nonce Bias

auteur

Diego Aranha, Pierre-Alain Fouque, Benoit Gérard, Jean-Gabriel Kammerer, Mehdi Tibouchi, Jean-Christophe Zapalowicz

article

Advances in Cryptology – ASIACRYPT 2014 – 20th International Conference on the Theory and Application of Cryptology and Information Security, Dec 2014, Kaoshiung, Taiwan. pp.262-281, ⟨10.1007/978-3-662-45611-8_14⟩

Accès au texte intégral et bibtex

titre

Synthesis of Fault Attacks on Cryptographic Implementations

auteur

Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz

article

ACM CCS 2014, Nov 2014, Scottsdale, United States. pp.16, ⟨10.1145/2660267.2660304⟩

Accès au texte intégral et bibtex

titre

System-level Non-interference for Constant-time Cryptography

auteur

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie

article

ACM SIGSAC Conference on Computer and Communications Security, CCS’14, Nov 2014, Scottsdale, United States. pp.1267 – 1279, ⟨10.1145/2660267.2660283⟩

Accès au texte intégral et bibtex

titre

Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach

auteur

Frédéric Besson, Nataliia Bielova, Thomas Jensen

article

Nordic Conference on Secure IT Systems (NordSec 2014), Oct 2014, Tromsø, Norway. ⟨10.1007/978-3-319-11599-3_11⟩

Accès au texte intégral et bibtex

titre

Making RSA–PSS Provably Secure against Non-random Faults

auteur

Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Mehdi Tibouchi, Jean-Christophe Zapalowicz, Benjamin Grégoire

article

Cryptographic Hardware and Embedded Systems – {CHES} 2014, Sep 2014, Busan, South Korea. pp.206 – 222, ⟨10.1007/978-3-662-44709-3_12⟩

Accès au texte intégral et bibtex

titre

A Probabilistic Framework for Security Scenarios with Dependent Actions

auteur

Barbara Kordy, Marc Pouly, Patrick Schweitzer

article

Integrated Formal Methods, Sep 2014, Bertinoro, Italy. pp.256 – 271, ⟨10.1007/978-3-319-10181-1_16⟩

Accès au texte intégral et bibtex

titre

Improving static analyses of C programs with conditional predicates

auteur

Sandrine Blazy, David Bühler, Boris Yakobowski

article

FMICS 2014: Formal Methods for Industrial Critical Systems, Sep 2014, Florence, Italy. pp.15, ⟨10.1007/978-3-319-10702-8_10⟩

Accès au bibtex

titre

Binary Elligator Squared

auteur

Diego Aranha, Pierre-Alain Fouque, Chen Qian, Mehdi Tibouchi, Jean-Christophe Zapalowicz

article

Selected Areas in Cryptography 2014, Aug 2014, Montreal, Canada. pp.17, ⟨10.1007/978-3-319-13051-4_2⟩

Accès au texte intégral et bibtex

titre

Statistical Properties of Short RSA Distribution and Their Cryptographic Applications

auteur

Pierre-Alain Fouque, Jean-Christophe Zapalowicz

article

Computing and Combinatorics, Aug 2014, Atlanta, United States. pp.525 – 536, ⟨10.1007/978-3-319-08783-2_45⟩

Accès au texte intégral et bibtex

titre

A Formally Verified WCET Estimation Tool

auteur

André Oliveira Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut

article

14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. ⟨10.4230/OASIcs.WCET.2014.11⟩

Accès au bibtex

titre

Towards Static Analysis of Functional Programs Using Tree Automata Completion

auteur

Thomas Genet

article

Workshop on Rewriting Logic and its Applications, Santiago Escobar, Apr 2014, Grenoble, France. pp.147 – 161, ⟨10.1007/978-3-319-12904-4_8⟩

Accès au texte intégral et bibtex

titre

Measuring the Robustness of Source Program Obfuscation – Studying the Impact of Compiler Optimizations on the Obfuscation of C Programs

auteur

Sandrine Blazy, Stéphanie Riaud

article

Fourth ACM Conference on Data and Application Security and Privacy – SIGSAC ACM CODASPY 2014, Mar 2014, San Antonio, United States

Accès au texte intégral et bibtex

titre

A Trusted Mechanised JavaScript Specification

auteur

Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith

article

POPL 2014 – 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States

Accès au texte intégral et bibtex

titre

Pretty-big-step-semantics-based Certified Abstract Interpretation

auteur

Martin Bodin, Thomas Jensen, Alan Schmitt

article

JFLA – 25ème Journées Francophones des Langages Applicatifs – 2014, Jan 2014, Fréjus, France

Accès au texte intégral et bibtex

titre

De la KAM avec un Processus d’Ordre Supérieur

auteur

Damien Pous, Alan Schmitt

article

JFLAs 2014, Jan 2014, Fréjus, France. pp.1-12

Accès au texte intégral et bibtex

titre

SawjaCard: A Static Analysis Tool for Certifying Java Card Applications

auteur

Frédéric Besson, Thomas Jensen, Pierre Vittet

article

21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. pp.51 – 67, ⟨10.1007/978-3-319-10936-7_4⟩

Accès au texte intégral et bibtex

titre

A Precise and Abstract Memory Model for C Using Symbolic Values

auteur

Frédéric Besson, Sandrine Blazy, Pierre Wilke

article

12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. pp.449 – 468, ⟨10.1007/978-3-319-12736-1_24⟩

Accès au texte intégral et bibtex

titre

A Verified Information-Flow Architecture

auteur

Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach

article

41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. ⟨10.1145/2535838.2535839⟩

Accès au bibtex

titre

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code

auteur

Sandrine Blazy, Vincent Laporte, David Pichardie

article

The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. pp.128 – 143, ⟨10.1007/978-3-319-08970-6_9⟩

Accès au texte intégral et bibtex

Book sections

titre

The CompCert memory model

auteur

Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart

article

Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010

Accès au bibtex

Master thesis

titre

Security analysis of Android applications

auteur

Bertrand Bonnefoy-Claudet

article

Formal Languages and Automata Theory [cs.FL]. 2014

Accès au texte intégral et bibtex

Reports

titre

A Note on the Precision of the Tree Automata Completion

auteur

Thomas Genet

article

[Research Report] IRISA. 2014, pp.13

Accès au texte intégral et bibtex

titre

Enforcing Browser Anonymity with Quantitative Information Flow

auteur

Frédéric Besson, Nataliia Bielova, Thomas Jensen

article

[Research Report] RR-8532, INRIA. 2014

Accès au texte intégral et bibtex

Theses

titre

Security of the pseudorandom number generators and implementations of public key signature schemes

auteur

Jean-Christophe Zapalowicz

article

Cryptography and Security [cs.CR]. Université de Rennes, 2014. English. ⟨NNT : 2014REN1S103⟩

Accès au texte intégral et bibtex

titre

Tree automata extensions for verification of infinite states systems

auteur

Valérie Murat

article

Performance et fiabilité [cs.PF]. Université de Rennes, 2014. Français. ⟨NNT : 2014REN1S033⟩

Accès au texte intégral et bibtex

2013

Journal articles

titre

A certified lightweight non-interference Java bytecode verifier

auteur

Gilles Barthe, David Pichardie, Tamara Rezk

article

Mathematical Structures in Computer Science, 2013, 23 (5), pp.1032-1081. ⟨10.1017/S0960129512000850⟩

Accès au texte intégral et bibtex

titre

Survey on JavaScript Security Policies and their Enforcement Mechanisms in a Web Browser

auteur

Nataliia Bielova

article

Journal of Logic and Algebraic Programming, 2013, Automated Specification and Verification of Web Systems, 82 (8), pp.243-262. ⟨10.1016/j.jlap.2013.05.001⟩

Accès au bibtex

Conference papers

titre

Recovering Private Keys Generated with Weak PRNGs

auteur

Pierre-Alain Fouque, Mehdi Tibouchi, Jean-Christophe Zapalowicz

article

Cryptography and Coding – 14th {IMA} International Conference, Dec 2013, Oxford, United Kingdom. pp.158 – 172, ⟨10.1007/978-3-642-45239-0_10⟩

Accès au texte intégral et bibtex

titre

Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq

auteur

Jael Kriener, Andy King, Sandrine Blazy

article

15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Sep 2013, Madrid, Spain. pp.37-48

Accès au texte intégral et bibtex

titre

Practical Pairwise Testing for Software Product Lines

auteur

Dusica Marijan, Arnaud Gotlieb, Sagar Sen, Aymeric Hervieu

article

SPLC 2013, Aug 2013, Tokyo, Japan

Accès au texte intégral et bibtex

titre

A completion algorithm for lattice tree automata

auteur

Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat

article

CIAA 2013 – 18th International Conference on Implementation and Application of Automata, Jul 2013, Halifax, NS, Canada. pp.134-145, ⟨10.1007/978-3-642-39274-0_13⟩

Accès au bibtex

titre

Time/Memory/Data Tradeoffs for Variants of the RSA Problem

auteur

Pierre-Alain Fouque, Damien Vergnaud, Jean-Christophe Zapalowicz

article

Computing and Combinatorics, 19th International Conference, COCOON 2013, Jun 2013, Hangzhou, China. pp.651-662, ⟨10.1007/978-3-642-38768-5_57⟩

Accès au texte intégral et bibtex

titre

Formal Verification of a C Value Analysis Based on Abstract Interpretation

auteur

Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie

article

SAS – 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344

Accès au texte intégral et bibtex

titre

Formal Verification of Loop Bound Estimation for WCET Analysis

auteur

Sandrine Blazy, André Maroneze, David Pichardie

article

VSTTE – Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303

Accès au texte intégral et bibtex

titre

Concurrent Flexible Reversibility

auteur

Ivan Lanese, Michaël Lienhardt, Claudio Antares Mezzina, Alan Schmitt, Jean-Bernard Stefani

article

22nd European Symposium on Programming, ESOP 2013, Mar 2013, Rome, Italy. pp.370-390, ⟨10.1007/978-3-642-37036-6_21⟩

Accès au texte intégral et bibtex

titre

Symbolic Path-Oriented Test Data Generation for Floating-Point Programs

auteur

Roberto Bagnara, Matthieu Carlier, Roberta Gori, Arnaud Gotlieb

article

Proc. of the 6th IEEE Int. Conf. on Software Testing, Verification and Validation (ICST’13), Mar 2013, Luxembourg, Luxembourg

Accès au texte intégral et bibtex

titre

A Certified JavaScript Interpreter

auteur

Martin Bodin, Alan Schmitt

article

JFLA – Journées francophones des langages applicatifs, Damien Pous and Christine Tasson, Feb 2013, Aussois, France

Accès au texte intégral et bibtex

titre

Plan B: A Buffered Memory Model for Java

auteur

Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, Jan Vitek

article

Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Jan 2013, Rome, Italy

Accès au bibtex

titre

Hybrid Information Flow Monitoring Against Web Tracking

auteur

Frédéric Besson, Nataliia Bielova, Thomas Jensen

article

CSF – 2013 IEEE 26th Computer Security Foundations Symposium, 2013, New Orleans, United States. ⟨10.1109/CSF.2013.23⟩

Accès au texte intégral et bibtex

titre

Result Certification of Static Program Analysers with Automated Theorem Provers

auteur

Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen

article

VSTTE 2013 – Fifth Working Conference on Verified Software: Theories, Tools and Experiments, 2013, Atherthon, United States

Accès au texte intégral et bibtex

Books

titre

Interactive Theorem Proving – 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings

auteur

Sandrine Blazy, Christine Paulin-Mohring, David Pichardie

article

Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Springer, 7998, pp.500, 2013, Lecture Notes in Computer Science, ⟨10.1007/978-3-642-39634-2⟩

Accès au bibtex

Reports

titre

Towards Static Analysis of Functional Programs using Tree Automata Completion

auteur

Thomas Genet

article

[Research Report] 2013, pp.15

Accès au texte intégral et bibtex

titre

Reachability Analysis of Innermost Rewriting

auteur

Thomas Genet, Yann Salmon

article

[Research Report] 2013

Accès au texte intégral et bibtex

titre

Tree Automata Completion for Static Analysis of Functional Programs

auteur

Thomas Genet, Yann Salmon

article

2013

Accès au texte intégral et bibtex

titre

Scenario realizability with constraint optimization

auteur

Rouwaida Abdallah, Arnaud Gotlieb, Loïc Hélouët, Claude Jard

article

[Research Report] 2013

Accès au texte intégral et bibtex

Theses

titre

Static analysis of numerical properties in the presence of pointers

auteur

Zhoulai Fu

article

Other [cs.OH]. Université de Rennes; Université européenne de Bretagne (2007-2016), 2013. English. ⟨NNT : 2013REN1S060⟩

Accès au texte intégral et bibtex

titre

Certification of static analysis in many-sorted first-order logic

auteur

Pierre-Emmanuel Cornilleau

article

Other [cs.OH]. École normale supérieure de Cachan – ENS Cachan, 2013. English. ⟨NNT : 2013DENS0012⟩

Accès au texte intégral et bibtex

2012

Journal articles

titre

Secure the Clones

auteur

Thomas Jensen, Florent Kirchner, David Pichardie

article

Logical Methods in Computer Science, 2012, 8 (2)

Accès au texte intégral et bibtex

titre

À propos des compilateurs

auteur

Sandrine Blazy, Joanna Jongwane

article

Interstices, 2012

Accès au bibtex

titre

Control-flow analysis of function calls and returns by abstract interpretation

auteur

Jan Midtgaard, Thomas Jensen

article

Information and Computation, 2012, 2012, pp.49-76. ⟨10.1016/j.ic.2011.11.005⟩

Accès au texte intégral et bibtex

Conference papers

titre

Managing Execution Environment Variability during Software Testing: An Industrial Experience

auteur

Aymeric Hervieu, Benoit Baudry, Arnaud Gotlieb

article

24th International Conference on Testing Software and Systems (ICTSS), Nov 2012, Aalborg, Denmark. pp.24-38, ⟨10.1007/978-3-642-34691-0_4⟩

Accès au texte intégral et bibtex

titre

Equational Abstraction Refinement for Certified Tree Regular Model Checking

auteur

Yohan Boichut, Benoit Boyer, Thomas Genet, Axel Legay

article

ICFEM, Nov 2012, Kyoto, Japan. pp.299-315

Accès au texte intégral et bibtex

titre

Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases

auteur

David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner

article

SAS – 19th International Static Analysis Symposium – 2012, Sep 2012, Deauville, France

Accès au bibtex

titre

Attacking RSA–CRT Signatures with Faults on Montgomery Multiplication

auteur

Pierre-Alain Fouque, Nicolas Guillermin, Delphine Leresteux, Mehdi Tibouchi, Jean-Christophe Zapalowicz

article

Cryptographic Hardware and Embedded Systems – {CHES} 2012, Sep 2012, Leuven, Belgium. pp.16, ⟨10.1007/978-3-642-33027-8_26⟩

Accès au texte intégral et bibtex

titre

Constraint-based reachability

auteur

Arnaud Gotlieb, Tristan Denmat, Nadjib Lazaar

article

Infinity workshop 2012, Aug 2012, Paris, France. ⟨10.4204/EPTCS.107.4⟩

Accès au texte intégral et bibtex

titre

Towards a formally verified obfuscating compiler

auteur

Sandrine Blazy, Roberto Giacobazzi

article

SSP 2012 – 2nd ACM SIGPLAN Software Security and Protection Workshop, ACM SIGPLAN, Jun 2012, Beijing, China

Accès au texte intégral et bibtex

titre

Perception de l’espace d’action chez les patients hémiplégiques

auteur

Michèle Carlier, A. Poulain, C. Bachelet, J. Labire, Yves Martin, H. Sassaini, Régis Levasseur, Yann Coello, Angela Bartolo

article

Symposium International de Neuropsychologie: Rehabilitation Cognitive et prise en charge chirurgicale, Jun 2012, Lille, France

Accès au bibtex

titre

Inferring Sequences Produced by Nonlinear Pseudorandom Number Generators Using Coppersmith’s Methods

auteur

Aurélie Bauer, Damien Vergnaud, Jean-Christophe Zapalowicz

article

PKC 2012 – 15th International Conference on Practice and Theory in Public Key Cryptography, May 2012, Darmstadt, Germany. pp.609-626, ⟨10.1007/978-3-642-30057-8_36⟩

Accès au bibtex

titre

Tightly-Secure Signatures from Lossy Identification Schemes

auteur

Michel Abdalla, Pierre-Alain Fouque, Vadim Lyubashevsky, Mehdi Tibouchi

article

Advances in Cryptology – {EUROCRYPT} 2012, Apr 2012, Cambridge, United Kingdom. pp.19, ⟨10.1007/978-3-642-29011-4_34⟩

Accès au texte intégral et bibtex

titre

A Formally Verified SSA-based Middle-end

auteur

Gilles Barthe, Delphine Demange, David Pichardie

article

21th European Symposium on Programming, ESOP 2012, Mar 2012, Tallin, Estonia. pp.47-66, ⟨10.1007/978-3-642-28869-2_3⟩

Accès au bibtex

titre

Formalisation de HOCore en Coq

auteur

Simon Boulier, Alan Schmitt

article

JFLA – Journées Francophones des Langages Applicatifs – 2012, Feb 2012, Carnac, France

Accès au texte intégral et bibtex

titre

Formally verified optimizing compilation in ACG-based flight control software

auteur

Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris

article

ERTS2 2012: Embedded Real Time Software and Systems, AAAF, SEE, Feb 2012, Toulouse, France

Accès au texte intégral et bibtex

titre

Proving Reachability Properties on Term Rewriting Systems with Strategies

auteur

Thomas Genet, Yann Salmon

article

Workshop on Strategies in Rewriting, Proving and Programming, 2012, London, United Kingdom

Accès au texte intégral et bibtex

Habilitation à diriger des recherches

titre

Toward a Verified Software Toolchain for Java

auteur

David Pichardie

article

Computer Science [cs]. ENS Cachan, 2012

Accès au bibtex

Master thesis

titre

Vérification probabiliste de résultats d’analyse statique

auteur

Antoine Bride

article

Informatique et langage [cs.CL]. 2012

Accès au texte intégral et bibtex

Reports

titre

Logical Combinators for Rich Type Systems

auteur

Pierre Genevès, Nabil Layaïda, Alan Schmitt

article

[Research Report] RR-8010, INRIA. 2012, pp.18

Accès au texte intégral et bibtex

titre

The CompCert Memory Model, Version 2

auteur

Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart

article

[Research Report] RR-7987, INRIA. 2012, pp.26

Accès au texte intégral et bibtex

titre

Tree Regular Model Checking for Lattice-Based Automata

auteur

Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat

article

[Technical Report] RT-0424, INRIA. 2012, pp.33

Accès au texte intégral et bibtex

Theses

titre

Semantic foundations of intermediate program representations

auteur

Delphine Demange

article

Other [cs.OH]. École normale supérieure de Cachan – ENS Cachan, 2012. English. ⟨NNT : 2012DENS0053⟩

Accès au texte intégral et bibtex

titre

Static analysis with dioids and polynomial ideals

auteur

Arnaud Jobin

article

Autre [cs.OH]. École normale supérieure de Cachan – ENS Cachan, 2012. Français. ⟨NNT : 2012DENS0004⟩

Accès au texte intégral et bibtex

Preprints, Working Papers, …

titre

Proofs as Cryptography: a new interpretation of the Curry-Howard isomorphism for software certificates

auteur

Amrit Kumar, Pierre-Alain Fouque, Thomas Genet, Mehdi Tibouchi

article

2012

Accès au texte intégral et bibtex

2011

Journal articles

titre

On the Expressiveness and Decidability of Higher-Order Process Calculi

auteur

Ivan Lanese, Jorge A Perez, Davide Sangiorgi, Alan Schmitt

article

Information and Computation, 2011, 209 (2), pp.29. ⟨10.1016/j.ic.2010.10.001⟩

Accès au texte intégral et bibtex

titre

Programming a certified abstract interpreter in constructive logic

auteur

David Cachera, David Pichardie

article

Revue des Sciences et Technologies de l’Information – Série TSI : Technique et Science Informatiques, 2011, pp.28. ⟨10.3166/tsi.30.381-408⟩

Accès au bibtex

Conference papers

titre

PACOGEN : Automatic Generation of Pairwise Test Configurations from Feature Models

auteur

Aymeric Hervieu, Benoit Baudry, Arnaud Gotlieb

article

Proc. of Int. Symp. on Soft. Reliability Engineering (ISSRE’11), Nov 2011, Hiroshima, Japan

Accès au texte intégral et bibtex

titre

Filtering by ULP Maximum

auteur

Matthieu Carlier, Arnaud Gotlieb

article

Proc. of the IEEE Int. Conf. on Tools for Artificial Intelligence (ICTAI’11), Nov 2011, Floride, United States

Accès au texte intégral et bibtex

titre

Characterizing Conclusive Approximations by Logical Formulae

auteur

Yohan Boichut, Thi-Bich-Hanh Dao, Valérie Murat

article

Reachability Problems 2011, Sep 2011, Gênes, Italy

Accès au texte intégral et bibtex

titre

A Nelson-Oppen based Proof System using Theory Specific Proof Systems

auteur

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie

article

First International Workshop on Proof eXchange for Theorem Proving – PxTP 2011, Aug 2011, Wrocław, Poland

Accès au texte intégral et bibtex

titre

A Flexible Proof Format for SMT: a Proposal

auteur

Frédéric Besson, Pascal Fontaine, Laurent Théry

article

First International Workshop on Proof eXchange for Theorem Proving – PxTP 2011, Aug 2011, Wrocław, Poland

Accès au texte intégral et bibtex

titre

Secure the Clones – Static Enforcement of Policies for Secure Object Copying

auteur

Thomas Jensen, Florent Kirchner, David Pichardie

article

ESOP 2011, 2011, Saarbrucken, Germany

Accès au texte intégral et bibtex

titre

Modular SMT Proofs for Fast Reflexive Checking inside Coq

auteur

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie

article

First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan

Accès au texte intégral et bibtex

Habilitation à diriger des recherches

titre

Contributions to Constraint-Based Testing

auteur

Arnaud Gotlieb

article

Génie logiciel [cs.SE]. Université Européenne de Bretagne, 2011

Accès au texte intégral et bibtex

Reports

titre

Formal Verification of an SSA-based Middle-end for CompCert

auteur

Gilles Barthe, Delphine Demange, David Pichardie

article

[University works] 2011

Accès au texte intégral et bibtex

titre

Negation for Free!

auteur

Nadjib Lazaar, Nourredine Aribi, Arnaud Gotlieb, Yahia Lebbah

article

[Research Report] RR-7749, INRIA. 2011, pp.16

Accès au texte intégral et bibtex

titre

Fast inference of polynomial invariants for imperative programs

auteur

David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner

article

[Research Report] RR-7627, INRIA. 2011, pp.31

Accès au texte intégral et bibtex

2010

Journal articles

titre

A Uniform Random Test Data Generator for Path Testing

auteur

Arnaud Gotlieb, Matthieu Petit

article

Journal of Systems and Software, 2010, 83 (12), pp.2618-2626. ⟨10.1016/j.jss.2010.08.021⟩

Accès au texte intégral et bibtex

titre

Long-Run Cost Analysis by Approximation of Linear Operators over Dioids

auteur

David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin

article

Mathematical Structures in Computer Science, 2010, 20 (4), pp.589-624. ⟨10.1017/S0960129510000113⟩

Accès au bibtex

titre

Equational Approximations for Tree Automata Completion

auteur

Thomas Genet, Vlad Rusu

article

Journal of Symbolic Computation, 2010, 45(5):574-597, May 2010 (5), pp.574-597

Accès au texte intégral et bibtex

titre

Verifying Resource Access Control on Mobile Interactive Devices

auteur

Frédéric Besson, Guillaume Dufaye, Thomas Jensen, David Pichardie

article

Journal of Computer Security, 2010, 18 (6), pp.971-998

Accès au texte intégral et bibtex

Conference papers

titre

Constraint-Based Test Input Generation for Java Bytecode

auteur

Florence Charreteur, Arnaud Gotlieb

article

Proc. of the 21st IEEE Int. Symp. on Softw. Reliability Engineering (ISSRE’10), Nov 2010, San Jose, CA, USA, United States

Accès au texte intégral et bibtex

titre

Constraint solving on modular integers

auteur

Arnaud Gotlieb, Michel Leconte, Bruno Marre

article

ModRef Worksop, associated to CP’2010, Sep 2010, Saint-Andrews, United Kingdom

Accès au texte intégral et bibtex

titre

On Testing Constraint Programs

auteur

Nadjib Lazaar, Arnaud Gotlieb, Yahia Lebbah

article

16th Int. Conf. on Principles and Practices of Constraint Programming (CP’2010), Sep 2010, St Andrews, Scotland, United Kingdom

Accès au texte intégral et bibtex

titre

Constraint Reasoning in FocalTest

auteur

Mathieu Carlier, Catherine Dubois, Arnaud Gotlieb

article

ICSOFT, Jul 2010, Athènes, Greece

Accès au texte intégral et bibtex

titre

Explanation-based generalization of infeasible path

auteur

Mickaël Delahaye, Bernard Botella, Arnaud Gotlieb

article

3rd IEEE International Conference on Software Testing, Validation and Verification (ICST’10), Apr 2010, Paris, France

Accès au texte intégral et bibtex

titre

Formal Verification of Coalescing Graph-Coloring Register Allocation

auteur

Sandrine Blazy, Benoît Robillard, Andrew W. W. Appel

article

19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. pp.145-164

Accès au texte intégral et bibtex

titre

Certified Result Checking for Polyhedral Analysis of Bytecode Programs

auteur

Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin

article

The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany

Accès au texte intégral et bibtex

titre

Sawja: Static Analysis Workshop for Java

auteur

Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin

article

The International Conference on Formal Verification of Object-Oriented Software, Beckert, Bernhard and Marché, Claude, 2010, Paris, France. pp.253–267

Accès au texte intégral et bibtex

titre

Enforcing Secure Object Initialization in Java

auteur

Laurent Hubert, Thomas Jensen, Vincent Monfort, David Pichardie

article

15th European Symposium on Research in Computer Security (ESORICS), 2010, Athènes, Greece. pp.101-115

Accès au texte intégral et bibtex

titre

A Provably Correct Stackless Intermediate Representation for Java Bytecode

auteur

Delphine Demange, Thomas Jensen, David Pichardie

article

The 8th Asian Symposium on Programming Languages and Systems (APLAS), 2010, Shangai, China

Accès au texte intégral et bibtex

titre

A Certified Denotational Abstract Interpreter

auteur

David Cachera, David Pichardie

article

International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. pp.9-24

Accès au texte intégral et bibtex

titre

Sécurité de la plate-forme d’exécution Java : limites et propositions d’améliorations

auteur

Guillaume Hiet, Frédéric Guihéry, Goulven Guiheux, David Pichardie, Christian Brunette

article

Symposium sur la sécurité des technologies de l’information et des communications (SSTIC), 2010, Rennes, France

Accès au texte intégral et bibtex

titre

Fault Localization in Constraint Programs

auteur

Nadjib Lazaar, Arnaud Gotlieb, Yahia Lebbah

article

22th Int. Conf. on Tools with Artificial Intelligence (ICTAI’2010), 2010, Arras, France

Accès au texte intégral et bibtex

titre

On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver

auteur

Frédéric Besson

article

8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh, United Kingdom

Accès au texte intégral et bibtex

Reports

titre

Equational Abstraction Refinement for Certified Tree Regular Model Checking

auteur

Yohan Boichut, Benoît Boyer, Thomas Genet, Axel Legay

article

[Technical Report] 2010

Accès au texte intégral et bibtex

titre

On Testing Constraint Programs

auteur

Nadjib Lazaar, Arnaud Gotlieb, Lebbah Yahia

article

[Research Report] RR-7291, INRIA. 2010

Accès au texte intégral et bibtex

titre

A Provably Correct Stackless Intermediate Representation For Java Bytecode

auteur

Delphine Demange, Thomas Jensen, David Pichardie

article

[Research Report] RR-7021, INRIA. 2010, pp.59

Accès au texte intégral et bibtex

Theses

titre

Constraint modeling of Java bytecode programs for auomatic test data generation

auteur

Florence Charreteur

article

Informatique [cs]. Université Européenne de Bretagne, 2010. Français. ⟨NNT : ⟩

Accès au texte intégral et bibtex

2009

Journal articles

titre

Modelling Dynamic Memory Management in Constraint-Based Testing

auteur

Florence Charreteur, Bernard Botella, Arnaud Gotlieb

article

Journal of Systems and Software, 2009, 82 (11), pp.1755-1766. ⟨10.1016/j.jss.2009.06.029⟩

Accès au texte intégral et bibtex

titre

Soundly Handling Static Fields: Issues, Semantics and Analysis

auteur

Laurent Hubert, David Pichardie

article

Electronic Notes in Theoretical Computer Science, 2009, Proceedings of the Fourth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2009), 253 (5), pp.15 – 30. ⟨10.1016/j.entcs.2009.11.012⟩

Accès au texte intégral et bibtex

Conference papers

titre

Control-flow analysis of function call and returns by abstract interpretation

auteur

Jan Midtgaard, Thomas Jensen

article

ACM International Conference on Functional Programming, Sep 2009, Edinburgh, United Kingdom. ⟨10.1145/1596550.1596592⟩

Accès au texte intégral et bibtex

titre

Vers une Théorie du Test des programmes à contraintes

auteur

Nadjib Lazaar, Arnaud Gotlieb, Yahia Lebbah

article

Cinquièmes Journées Francophones de Programmation par Contraintes, Orléans, juin 2009, Jun 2009, France. pp.65-75

Accès au texte intégral et bibtex

titre

Constraint Based Strategies

auteur

Helene Kirchner, Kirchner Florent, Claude Kirchner

article

18th International Workshop on Functional and Constraint Logic Programming – WFLP 2009, Jun 2009, Brasilia, Brazil. pp.13-26

Accès au bibtex

titre

Distinguish Dynamic Basic Blocks by Structural Statistical Testing

auteur

Matthieu Petit, Arnaud Gotlieb

article

12th European Workshop on Dependable Computing, EWDC 2009, May 2009, Toulouse, France. 8 p

Accès au texte intégral et bibtex

titre

A Certified Data Race Analysis for a Java-like Language

auteur

Frédéric Dabrowski, David Pichardie

article

TPHOL’09, 2009, Germany. pp.212–227

Accès au bibtex

titre

Verifying Temporal Regular properties of Abstractions of Term Rewriting Systems

auteur

Benoît Boyer, Thomas Genet

article

RULE’09, 2009, France. pp.99-108

Accès au texte intégral et bibtex

titre

Comparing Techniques for Certified Static Analysis

auteur

David Cachera, David Pichardie

article

The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. pp.111-115

Accès au texte intégral et bibtex

titre

CPA beats oo-CFA

auteur

Frédéric Besson

article

FTfJP ’09 – Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, 2009, Genova, Italy. ⟨10.1145/1557898.1557905⟩

Accès au texte intégral et bibtex

titre

Certified Static Analysis by Abstract Interpretation

auteur

Frédéric Besson, David Cachera, Thomas Jensen, David Pichardie

article

Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. pp.223-257

Accès au texte intégral et bibtex

titre

On the Unobservability of a Trust Relation in Mobile Ad Hoc Networks

auteur

Olivier Heen, Gilles Guette, Thomas Genet

article

Information Security Theory and Practice. Smart Devices, Pervasive Systems, and Ubiquitous Networks, 2009, Belgium. pp.1-11

Accès au texte intégral et bibtex

Habilitation à diriger des recherches

titre

Reachability analysis of rewriting for software verification

auteur

Thomas Genet

article

Software Engineering [cs.SE]. Université Rennes 1, 2009

Accès au texte intégral et bibtex

Reports

titre

Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation

auteur

Jan Midtgaard, Thomas P. Jensen

article

[Research Report] RR-6681, INRIA. 2009

Accès au texte intégral et bibtex

titre

Computing the Least Fix-point Semantics of Definite Logic Programs Using BDDs

auteur

Frédéric Besson, Thomas Jensen, Tiphaine Turpin

article

[Research Report] PI 1939, 2009, pp.25

Accès au texte intégral et bibtex

2008

Conference papers

titre

A Non-Null Annotation Inferencer for Java Bytecode

auteur

Laurent Hubert

article

PASTE: Program analysis for software tools and engineering, Nov 2008, Atlanta, Georgia, United States. pp.10.1145/1512475.1512484, ⟨10.1145/1512475.1512484⟩

Accès au texte intégral et bibtex

1999

Conference papers

titre

Polyhedral Analysis for Synchronous Languages

auteur

Frédéric Besson, Thomas Jensen, Jean-Pierre Talpin

article

6th International Symposium on Static Analysis (SAS’99), Sep 1999, Venice, Italy. pp.51-68

Accès au texte intégral et bibtex

1998

Journal articles

titre

Dynamic optimization of interval narrowing algorithms

auteur

Olivier Lhomme, Arnaud Gotlieb, Michel Rueher

article

Journal of Logic Programming, 1998, 37 (1-3), pp.165-183. ⟨10.1016/S0743-1066(98)10007-9⟩

Accès au texte intégral et bibtex