Edit Profile (opens in new tab) Pichardie, David Compute Distance To: Compute Author ID: pichardie.david Published as: Pichardie, David Documents Indexed: 30 Publications since 2001 2 Contributions as Editor Co-Authors: 40 Co-Authors with 31 Joint Publications 659 Co-Co-Authors all top 5 Co-Authors 1 single-authored 8 Cachera, David 7 Blazy, Sandrine 6 Demange, Delphine 4 Barthe, Gilles 4 Besson, Frédéric 4 Laporte, Vincent 3 Jagannathan, Suresh 3 Rusu, Vlad 3 Vitek, Jan 2 Kirchner, Florent 2 Petri, Gustavo 2 Rezk, Tamara 2 Zakowski, Yannick 1 Azevedo de Amorim, Arthur 1 Barré, Nicolas 1 Bertot, Yves 1 Betarte, Gustavo 1 Campo, Juan Diego 1 Collins, Nathan A. 1 Cornilleau, Pierre-Emmanuel 1 Dabrowski, Frédéric 1 DeHon, Andre 1 Forest, Julien 1 Franceschino, Lucas 1 Hriţcu, Cătălin 1 Hubert, Laurent 1 Léchenet, Jean-Christophe 1 Luna, Carlos 1 Mirliaz, Solène 1 Monfort, Vincent 1 Paulin-Mohring, Christine 1 Pierce, Benjamin C. 1 Pollack, Randy 1 Schneider, Gerardo 1 Sighireanu, Mihaela 1 Talpin, Jean-Pierre 1 Tolmach, Andrew 1 Trieu, Alix 1 Turpin, Tiphaine 1 Zhao, Lei Serials 3 Journal of Automated Reasoning 2 Theoretical Computer Science 2 Lecture Notes in Computer Science 1 MSCS. Mathematical Structures in Computer Science 1 Logical Methods in Computer Science Fields 32 Computer science (68-XX) 2 General and overarching topics; collections (00-XX) 2 Mathematical logic and foundations (03-XX) 1 Information and communication theory, circuits (94-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 22 Publications have been cited 86 times in 70 Documents Cited by ▼ Year ▼ Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant. Zbl 1185.68616Barthe, Gilles; Forest, Julien; Pichardie, David; Rusu, Vlad 11 2006 Formalizing convex hull algorithms. Zbl 1005.68557Pichardie, David; Bertot, Yves 9 2001 Proof-carrying code from certified abstract interpretation and fixpoint compression. Zbl 1153.68354Besson, Frédéric; Jensen, Thomas; Pichardie, David 7 2006 A verified information-flow architecture. Zbl 1284.68306Azevedo de Amorim, Arthur; Collins, Nathan; DeHon, André; Demange, Delphine; Hriţcu, Cătălin; Pichardie, David; Pierce, Benjamin C.; Pollack, Randy; Tolmach, Andrew 6 2014 Extracting a data flow analyser in constructive logic. Zbl 1077.68051Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad 6 2005 Certified memory usage analysis. Zbl 1120.68385Cachera, David; Jensen, Thomas; Pichardie, David; Schneider, Gerardo 5 2005 A certified denotational abstract interpreter. Zbl 1291.68331Cachera, David; Pichardie, David 5 2010 Building certified static analysers by modular construction of well-founded lattices. Zbl 1286.68401Pichardie, David 5 2008 A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112Barthe, Gilles; Pichardie, David; Rezk, Tamara 5 2007 Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Zbl 1268.68006 4 2013 Plan B, a buffered memory model for Java. Zbl 1301.68098Demange, Delphine; Laporte, Vincent; Zhao, Lei; Jagannathan, Suresh; Pichardie, David; Vitek, Jan 4 2013 Extracting a data flow analyser in constructive logic. Zbl 1126.68345Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad 3 2004 Verifying a concurrent garbage collector using a rely-guarantee methodology. Zbl 1468.68067Zakowski, Yannick; Cachera, David; Demange, Delphine; Petri, Gustavo; Pichardie, David; Jagannathan, Suresh; Vitek, Jan 3 2017 Sawja: static analysis workshop for Java. Zbl 1308.68028Hubert, Laurent; Barré, Nicolas; Besson, Frédéric; Demange, Delphine; Jensen, Thomas; Monfort, Vincent; Pichardie, David; Turpin, Tiphaine 3 2011 An abstract memory functor for verified C static analyzers. Zbl 1361.68058Blazy, Sandrine; Laporte, Vincent; Pichardie, David 2 2016 System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David 2 2020 Modular SMT proofs for fast reflexive checking inside Coq. Zbl 1350.68224Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David 1 2011 Embedding of systems of affine recurrence equations in Coq. Zbl 1279.68286Cachera, David; Pichardie, David 1 2003 Validating dominator trees for a fast, verified dominance test. Zbl 1466.68030Blazy, Sandrine; Demange, Delphine; Pichardie, David 1 2015 A certified data race analysis for a Java-like language. Zbl 1252.68054Dabrowski, Frédéric; Pichardie, David 1 2009 Secure the clones. Zbl 1238.68047Jensen, Thomas; Kirchner, Florent; Pichardie, David 1 2012 Secure the clones. Static enforcement of policies for secure object copying. Zbl 1326.68098Jensen, Thomas; Kirchner, Florent; Pichardie, David 1 2011 System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David 2 2020 Verifying a concurrent garbage collector using a rely-guarantee methodology. Zbl 1468.68067Zakowski, Yannick; Cachera, David; Demange, Delphine; Petri, Gustavo; Pichardie, David; Jagannathan, Suresh; Vitek, Jan 3 2017 An abstract memory functor for verified C static analyzers. Zbl 1361.68058Blazy, Sandrine; Laporte, Vincent; Pichardie, David 2 2016 Validating dominator trees for a fast, verified dominance test. Zbl 1466.68030Blazy, Sandrine; Demange, Delphine; Pichardie, David 1 2015 A verified information-flow architecture. Zbl 1284.68306Azevedo de Amorim, Arthur; Collins, Nathan; DeHon, André; Demange, Delphine; Hriţcu, Cătălin; Pichardie, David; Pierce, Benjamin C.; Pollack, Randy; Tolmach, Andrew 6 2014 Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Zbl 1268.68006 4 2013 Plan B, a buffered memory model for Java. Zbl 1301.68098Demange, Delphine; Laporte, Vincent; Zhao, Lei; Jagannathan, Suresh; Pichardie, David; Vitek, Jan 4 2013 Secure the clones. Zbl 1238.68047Jensen, Thomas; Kirchner, Florent; Pichardie, David 1 2012 Sawja: static analysis workshop for Java. Zbl 1308.68028Hubert, Laurent; Barré, Nicolas; Besson, Frédéric; Demange, Delphine; Jensen, Thomas; Monfort, Vincent; Pichardie, David; Turpin, Tiphaine 3 2011 Modular SMT proofs for fast reflexive checking inside Coq. Zbl 1350.68224Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David 1 2011 Secure the clones. Static enforcement of policies for secure object copying. Zbl 1326.68098Jensen, Thomas; Kirchner, Florent; Pichardie, David 1 2011 A certified denotational abstract interpreter. Zbl 1291.68331Cachera, David; Pichardie, David 5 2010 A certified data race analysis for a Java-like language. Zbl 1252.68054Dabrowski, Frédéric; Pichardie, David 1 2009 Building certified static analysers by modular construction of well-founded lattices. Zbl 1286.68401Pichardie, David 5 2008 A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112Barthe, Gilles; Pichardie, David; Rezk, Tamara 5 2007 Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant. Zbl 1185.68616Barthe, Gilles; Forest, Julien; Pichardie, David; Rusu, Vlad 11 2006 Proof-carrying code from certified abstract interpretation and fixpoint compression. Zbl 1153.68354Besson, Frédéric; Jensen, Thomas; Pichardie, David 7 2006 Extracting a data flow analyser in constructive logic. Zbl 1077.68051Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad 6 2005 Certified memory usage analysis. Zbl 1120.68385Cachera, David; Jensen, Thomas; Pichardie, David; Schneider, Gerardo 5 2005 Extracting a data flow analyser in constructive logic. Zbl 1126.68345Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad 3 2004 Embedding of systems of affine recurrence equations in Coq. Zbl 1279.68286Cachera, David; Pichardie, David 1 2003 Formalizing convex hull algorithms. Zbl 1005.68557Pichardie, David; Bertot, Yves 9 2001 all cited Publications top 5 cited Publications all top 5 Cited by 128 Authors 13 Pichardie, David 4 Beringer, Lennart 4 Dufourd, Jean-François 3 Besson, Frédéric 3 Blazy, Sandrine 3 Cachera, David 3 Krauss, Alexander 2 Albert, Elvira 2 Barthe, Gilles 2 Bauereiß, Thomas 2 Bertot, Yves 2 Bove, Ana 2 Chlipala, Adam J. 2 Dehlinger, Christophe 2 Demange, Delphine 2 Devriese, Dominique 2 Fava, Daniel Schnetzer 2 Fuhs, Carsten 2 Giesl, Jürgen 2 Hofmann, Martin 2 Laporte, Vincent 2 Leroy, Xavier 2 Marić, Filip 2 Pesenti Gritti, Armando 2 Popescu, Andrei 2 Puebla, Germán 2 Raimondi, Franco 2 Schneider-Kamp, Peter 2 Steffen, Martin 2 Stolz, Volker 2 Stratulat, Sorin 1 Aderhold, Markus 1 Allamigeon, Xavier 1 Åman Pohjola, Johannes 1 Arenas, Puri 1 Aschermann, Cornelius 1 Bacelar Almeida, José 1 Barbar, Mohamad 1 Barbosa, Manuel 1 Barré, Nicolas 1 Bengtson, Jesper 1 Bernhard, David 1 Birkedal, Lars 1 Boender, Jaap P. 1 Boutry, Pierre 1 Brockschmidt, Marc 1 Brookes, Stephen D. 1 Brun, Christophe 1 Cogumbreiro, Tiago 1 Cruz-Filipe, Luís 1 Dabrowski, Frédéric 1 Darais, David 1 Deng, Chaoqiang 1 Doczkal, Christian 1 Drămnesc, Isabela 1 Fallah, Mehran S. 1 Felsner, Stefan 1 Fischlin, Marc 1 Franceschino, Lucas 1 Frohn, Florian 1 Genaim, Samir 1 Grabowski, Robert 1 Grégoire, Thomas 1 Gurov, Dilian 1 Hainry, Emmanuel 1 Hensel, Jera 1 Heras, Jónathan 1 Hermenegildo, Manuel V. 1 Hölzl, Johannes 1 Hubert, Laurent 1 Huisman, Marieke 1 Immler, Fabian 1 Iranmanesh, Zeinab 1 Jagannathan, Suresh 1 Jakobs, Marie-Christine 1 Jebelean, Tudor 1 Jensen, Thomas P. 1 Jones, Cliff B. 1 Kammüller, Florian 1 Katz, Ricardo David 1 Kavanagh, Ryan 1 Kirchner, Florent 1 Komendantskaya, Ekaterina 1 Lange, Julien 1 Larsen, Kim Skak 1 Léchenet, Jean-Christophe 1 Magaud, Nicolas 1 Malecha, Gregory 1 Midtgaard, Jan 1 Mirliaz, Solène 1 Monfort, Vincent 1 Myreen, Magnus O. 1 Nagarajan, Rajagopal 1 Namjoshi, Kedar S. 1 Nipkow, Tobias 1 Pavlova, Mariela 1 Péchoux, Romain 1 Petri, Gustavo 1 Piessens, Frank 1 Pilz, Alexander ...and 28 more Authors all top 5 Cited in 16 Serials 16 Journal of Automated Reasoning 5 Theoretical Computer Science 4 Journal of Functional Programming 2 Journal of Symbolic Computation 2 Information and Computation 2 Computational Geometry 2 MSCS. Mathematical Structures in Computer Science 2 The Journal of Logic and Algebraic Programming 2 Computer Languages, Systems & Structures 1 New Generation Computing 1 Algorithmica 1 Formal Aspects of Computing 1 Formal Methods in System Design 1 Mathematics in Computer Science 1 Logical Methods in Computer Science 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 12 Fields 67 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 3 Numerical analysis (65-XX) 2 Convex and discrete geometry (52-XX) 2 Operations research, mathematical programming (90-XX) 2 Information and communication theory, circuits (94-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Ordinary differential equations (34-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Probability theory and stochastic processes (60-XX) 1 Quantum theory (81-XX) 1 Mathematics education (97-XX) Citations by Year