David Pichardie

84 papers A* 5A 8B 18Misc 2Journal 28Unranked 20

Year	Rank	Type	Title / Venue / Authors
2025	B	`conf`	Contextual Equality Saturation. SAS Alexandre Drewery, Thomas P. Jensen, David Pichardie
2025	J	`jnl`	Preface of the special issue on the static analysis symposium 2020 and 2022. Formal Methods Syst. Des. David Pichardie, Mihaela Sighireanu, Gagandeep Singh, Caterina Urban
2023	J	`jnl`	Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. Proc. ACM Program. Lang. Aurèle Barrière, Sandrine Blazy, David Pichardie
2023	J	`jnl`	Leveraging Static Analysis for Bug Repair. CoRR Ruba Mutasim, Gabriel Synnaeve, David Pichardie, Baptiste Rozière
2022	B	`conf`	A Flow-Insensitive-Complete Program Representation. VMCAI Solène Mirliaz, David Pichardie
2022	J	`jnl`	Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert Backend into a Formally Verified JIT Compiler. CoRR Aurèle Barrière, Sandrine Blazy, David Pichardie
2022	B	`conf`	Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. SAS Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe
2021	J	`jnl`	Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek
2021	A	`conf`	Secure Compilation of Constant-Resource Programs. CSF Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie
2021	B	`conf`	Verified Functional Programming of an Abstract Interpreter. SAS Lucas Franceschino, David Pichardie, Jean-Pierre Talpin
2021	J	`jnl`	Verified Functional Programming of an Abstract Interpreter. CoRR Lucas Franceschino, David Pichardie, Jean-Pierre Talpin
2020	—	`conf`	A Fast Verified Liveness Analysis in SSA Form. IJCAR (2) Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie
2020	J	`jnl`	Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2020	B	`ed.`	Static Analysis - 27th International Symposium, SAS 2020, Virtual Event, November 18-20, 2020, Proceedings SAS David Pichardie, Mihaela Sighireanu
2020	J	`jnl`	System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. J. Autom. Reason. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie
2019	J	`jnl`	Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2019	J	`jnl`	Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. J. Autom. Reason. Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
2019	J	`jnl`	Verifying constant-time implementations by abstract interpretation. J. Comput. Secur. Sandrine Blazy, David Pichardie, Alix Trieu
2018	J	`jnl`	Preface. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. David Pichardie, Mihaela Sighireanu
2018	B	`conf`	Semantic reasoning about the sea of nodes. CC Delphine Demange, Yon Fernández de Retana, David Pichardie
2018	Misc	`conf`	Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement. SAC Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie
2017	A	`conf`	Verified Translation Validation of Static Analyses. CSF Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu
2017	—	`conf`	Verifying Constant-Time Implementations by Abstract Interpretation. ESORICS (1) Sandrine Blazy, David Pichardie, Alix Trieu
2017	B	`conf`	Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. ITP Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
2016	J	`jnl`	A verified information-flow architecture. J. Comput. Secur. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
2016	—	`conf`	An Extended Buffered Memory Model With Full Reorderings. FTfJP@ECOOP Gurvan Cabon, David Cachera, David Pichardie
2016	A	`conf`	An abstract memory functor for verified C static analyzers. ICFP Sandrine Blazy, Vincent Laporte, David Pichardie
2016	J	`jnl`	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. J. Autom. Reason. Sandrine Blazy, Vincent Laporte, David Pichardie
2015	A*	`conf`	A Formally-Verified C Static Analyzer. POPL Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
2015	J	`jnl`	A Verified Information-Flow Architecture. CoRR Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
2015	B	`conf`	Validating Dominator Trees for a Fast, Verified Dominance Test. ITP Sandrine Blazy, Delphine Demange, David Pichardie
2015	B	`conf`	Verified Validation of Program Slicing. CPP Sandrine Blazy, André Maroneze, David Pichardie
2015	B	`conf`	Verifying Fast and Sparse SSA-Based Optimizations in Coq. CC Delphine Demange, David Pichardie, Léo Stefanesco
2014	—	`conf`	A Formally Verified WCET Estimation Tool. WCET André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut
2014	A*	`conf`	A verified information-flow architecture. POPL Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
2014	J	`jnl`	Atomicity Refinement for Verified Compilation. ACM Trans. Program. Lang. Syst. Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek
2014	A*	`conf`	Atomicity refinement for verified compilation. PLDI Suresh Jagannathan, Gustavo Petri, Jan Vitek, David Pichardie, Vincent Laporte
2014	J	`jnl`	Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst. Gilles Barthe, Delphine Demange, David Pichardie
2014	A*	`conf`	System-level Non-interference for Constant-time Cryptography. CCS Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, David Pichardie
2014	J	`jnl`	System-level non-interference for constant-time cryptography. IACR Cryptol. ePrint Arch. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie
2014	B	`conf`	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. ITP Sandrine Blazy, Vincent Laporte, David Pichardie
2013	J	`jnl`	A certified lightweight non-interference Java bytecode verifier. Math. Struct. Comput. Sci. Gilles Barthe, David Pichardie, Tamara Rezk
2013	—	`conf`	Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE Sandrine Blazy, André Maroneze, David Pichardie
2013	J	`jnl`	Formal Verification of a C Value Analysis Based on Abstract Interpretation CoRR Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
2013	B	`conf`	Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
2013	B	`ed.`	Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings ITP Sandrine Blazy, Christine Paulin-Mohring, David Pichardie
2013	A*	`conf`	Plan B: a buffered memory model for Java. POPL Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek
2012	A	`conf`	A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. ESOP Gilles Barthe, Delphine Demange, David Pichardie
2012	—	`ed.`	Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012 PxTP David Pichardie, Tjark Weber
2012	J	`jnl`	Secure the Clones Log. Methods Comput. Sci. Thomas P. Jensen, Florent Kirchner, David Pichardie
2012	—	`book`	Toward a Verified Software Toolchain for Java. David Pichardie
2011	—	`conf`	A Nelson-Oppen based Proof System using Theory Specific Proof Systems. PxTP Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
2011	B	`conf`	Modular SMT Proofs for Fast Reflexive Checking Inside Coq. CPP Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
2011	—	`ed.`	Proceedings of the Fifth Workshop on Bytecode Semantics, Verification, Analysis and Transformation, Bytecode@ETAPS 2010, Paphos, Cyprus, March 27, 2010 Bytecode@ETAPS David Pichardie
2011	J	`jnl`	Programmation d'un interpréteur abstrait certifié en logique constructive. Tech. Sci. Informatiques David Cachera, David Pichardie
2011	A	`conf`	Secure the Clones - Static Enforcement of Policies for Secure Object Copying. ESOP Thomas P. Jensen, Florent Kirchner, David Pichardie
2010	B	`conf`	A Certified Denotational Abstract Interpreter. ITP David Cachera, David Pichardie
2010	B	`conf`	A Provably Correct Stackless Intermediate Representation for Java Bytecode. APLAS Delphine Demange, Thomas P. Jensen, David Pichardie
2010	—	`conf`	Certified Result Checking for Polyhedral Analysis of Bytecode Programs. TGC Frédéric Besson, Thomas P. Jensen, David Pichardie, Tiphaine Turpin
2010	J	`jnl`	Enforcing Secure Object Initialization in Java CoRR Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie
2010	A	`conf`	Enforcing Secure Object Initialization in Java. ESORICS Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie
2010	—	`conf`	Preface. Bytecode@ETAPS David Pichardie
2010	J	`jnl`	Sawja: Static Analysis Workshop for Java CoRR Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
2010	—	`conf`	Sawja: Static Analysis Workshop for Java. FoVeOOS Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
2010	J	`jnl`	Soundly Handling Static Fields: Issues, Semantics and Analysis CoRR Laurent Hubert, David Pichardie
2010	J	`jnl`	Verifying resource access control on mobile interactive devices. J. Comput. Secur. Frédéric Besson, Guillaume Dufay, Thomas P. Jensen, David Pichardie
2009	—	`conf`	A Certified Data Race Analysis for a Java-like Language. TPHOLs Frédéric Dabrowski, David Pichardie
2009	—	`conf`	Certified Static Analysis by Abstract Interpretation. FOSAD Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie
2009	—	`conf`	Comparing Techniques for Certified Static Analysis. NASA Formal Methods David Cachera, David Pichardie
2009	—	`conf`	Soundly Handling Static Fields: Issues, Semantics and Analysis. BYTECODE@ETAPS Laurent Hubert, David Pichardie
2008	—	`conf`	Building Certified Static Analysers by Modular Construction of Well-founded Lattices. FICS David Pichardie
2008	B	`conf`	Preservation of Proof Pbligations for Hybrid Verification Methods. SEFM Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese
2008	—	`conf`	Semantic Foundations and Inference of Non-null Annotations. FMOODS Laurent Hubert, Thomas P. Jensen, David Pichardie
2007	A	`conf`	A Certified Lightweight Non-interference Java Bytecode Verifier. ESOP Gilles Barthe, David Pichardie, Tamara Rezk
2007	—	`conf`	The MOBIUS Proof Carrying Code Infrastructure. FMCO Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie
2006	Misc	`conf`	Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. FLOPS Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu
2006	J	`jnl`	Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. Frédéric Besson, Thomas P. Jensen, David Pichardie
2005	B	`conf`	Certified Memory Usage Analysis. FM David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider
2005	J	`jnl`	Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
2005	—	`conf`	Modular Proof Principles for Parameterised Concretizations. CASSIS David Pichardie
2004	A	`conf`	Extracting a Data Flow Analyser in Constructive Logic. ESOP David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
2003	—	`conf`	A Java Card CAP converter in PVS. COCV Thomas Genet, Thomas P. Jensen, Vikash Kodati, David Pichardie
2003	—	`conf`	Embedding of Systems of Affine Recurrence Equations in Coq. TPHOLs David Cachera, David Pichardie
2001	—	`conf`	Formalizing Convex Hull Algorithms. TPHOLs David Pichardie, Yves Bertot