×
Author ID: pichardie.david Recent zbMATH articles by "Pichardie, David"
Published as: Pichardie, David

Publications by Year

Citations contained in zbMATH Open

23 Publications have been cited 104 times in 88 Documents Cited by Year
Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant. Zbl 1185.68616
Barthe, Gilles; Forest, Julien; Pichardie, David; Rusu, Vlad
13
2006
Formalizing convex hull algorithms. Zbl 1005.68557
Pichardie, David; Bertot, Yves
13
2001
Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Zbl 1268.68006
8
2013
A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112
Barthe, Gilles; Pichardie, David; Rezk, Tamara
7
2007
Proof-carrying code from certified abstract interpretation and fixpoint compression. Zbl 1153.68354
Besson, Frédéric; Jensen, Thomas; Pichardie, David
7
2006
A verified information-flow architecture. Zbl 1284.68306
Azevedo 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.68051
Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad
6
2005
Building certified static analysers by modular construction of well-founded lattices. Zbl 1286.68401
Pichardie, David
5
2008
Certified memory usage analysis. Zbl 1120.68385
Cachera, David; Jensen, Thomas; Pichardie, David; Schneider, Gerardo
5
2005
A certified denotational abstract interpreter. Zbl 1291.68331
Cachera, David; Pichardie, David
5
2010
Plan B, a buffered memory model for Java. Zbl 1301.68098
Demange, Delphine; Laporte, Vincent; Zhao, Lei; Jagannathan, Suresh; Pichardie, David; Vitek, Jan
4
2013
Verifying a concurrent garbage collector using a rely-guarantee methodology. Zbl 1468.68067
Zakowski, Yannick; Cachera, David; Demange, Delphine; Petri, Gustavo; Pichardie, David; Jagannathan, Suresh; Vitek, Jan
4
2017
System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David
4
2020
Extracting a data flow analyser in constructive logic. Zbl 1126.68345
Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad
3
2004
Sawja: static analysis workshop for Java. Zbl 1308.68028
Hubert, Laurent; Barré, Nicolas; Besson, Frédéric; Demange, Delphine; Jensen, Thomas; Monfort, Vincent; Pichardie, David; Turpin, Tiphaine
3
2011
Validating dominator trees for a fast, verified dominance test. Zbl 1466.68030
Blazy, Sandrine; Demange, Delphine; Pichardie, David
2
2015
An abstract memory functor for verified C static analyzers. Zbl 1361.68058
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
2
2016
Modular SMT proofs for fast reflexive checking inside Coq. Zbl 1350.68224
Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David
2
2011
Verified abstract interpretation techniques for disassembling low-level self-modifying code. Zbl 1357.68041
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
1
2016
Secure the clones. Zbl 1238.68047
Jensen, Thomas; Kirchner, Florent; Pichardie, David
1
2012
A certified data race analysis for a Java-like language. Zbl 1252.68054
Dabrowski, Frédéric; Pichardie, David
1
2009
Secure the clones. Static enforcement of policies for secure object copying. Zbl 1326.68098
Jensen, Thomas; Kirchner, Florent; Pichardie, David
1
2011
Embedding of systems of affine recurrence equations in Coq. Zbl 1279.68286
Cachera, David; Pichardie, David
1
2003
System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David
4
2020
Verifying a concurrent garbage collector using a rely-guarantee methodology. Zbl 1468.68067
Zakowski, Yannick; Cachera, David; Demange, Delphine; Petri, Gustavo; Pichardie, David; Jagannathan, Suresh; Vitek, Jan
4
2017
An abstract memory functor for verified C static analyzers. Zbl 1361.68058
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
2
2016
Verified abstract interpretation techniques for disassembling low-level self-modifying code. Zbl 1357.68041
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
1
2016
Validating dominator trees for a fast, verified dominance test. Zbl 1466.68030
Blazy, Sandrine; Demange, Delphine; Pichardie, David
2
2015
A verified information-flow architecture. Zbl 1284.68306
Azevedo 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
8
2013
Plan B, a buffered memory model for Java. Zbl 1301.68098
Demange, Delphine; Laporte, Vincent; Zhao, Lei; Jagannathan, Suresh; Pichardie, David; Vitek, Jan
4
2013
Secure the clones. Zbl 1238.68047
Jensen, Thomas; Kirchner, Florent; Pichardie, David
1
2012
Sawja: static analysis workshop for Java. Zbl 1308.68028
Hubert, 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.68224
Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David
2
2011
Secure the clones. Static enforcement of policies for secure object copying. Zbl 1326.68098
Jensen, Thomas; Kirchner, Florent; Pichardie, David
1
2011
A certified denotational abstract interpreter. Zbl 1291.68331
Cachera, David; Pichardie, David
5
2010
A certified data race analysis for a Java-like language. Zbl 1252.68054
Dabrowski, Frédéric; Pichardie, David
1
2009
Building certified static analysers by modular construction of well-founded lattices. Zbl 1286.68401
Pichardie, David
5
2008
A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112
Barthe, Gilles; Pichardie, David; Rezk, Tamara
7
2007
Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant. Zbl 1185.68616
Barthe, Gilles; Forest, Julien; Pichardie, David; Rusu, Vlad
13
2006
Proof-carrying code from certified abstract interpretation and fixpoint compression. Zbl 1153.68354
Besson, Frédéric; Jensen, Thomas; Pichardie, David
7
2006
Extracting a data flow analyser in constructive logic. Zbl 1077.68051
Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad
6
2005
Certified memory usage analysis. Zbl 1120.68385
Cachera, David; Jensen, Thomas; Pichardie, David; Schneider, Gerardo
5
2005
Extracting a data flow analyser in constructive logic. Zbl 1126.68345
Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad
3
2004
Embedding of systems of affine recurrence equations in Coq. Zbl 1279.68286
Cachera, David; Pichardie, David
1
2003
Formalizing convex hull algorithms. Zbl 1005.68557
Pichardie, David; Bertot, Yves
13
2001
all top 5

Cited by 151 Authors

14 Pichardie, David
5 Dufourd, Jean-François
4 Barthe, Gilles
4 Beringer, Lennart
4 Cachera, David
4 Schneider-Kamp, Peter
3 Besson, Frédéric
3 Blazy, Sandrine
3 Cruz-Filipe, Luís
3 Demange, Delphine
3 Krauss, Alexander
2 Albert, Elvira
2 Allamigeon, Xavier
2 Bacelar Almeida, José
2 Barbosa, Manuel
2 Bauereiß, Thomas
2 Bertot, Yves
2 Bove, Ana
2 Chlipala, Adam J.
2 Dehlinger, Christophe
2 Devriese, Dominique
2 Fava, Daniel Schnetzer
2 Felsner, Stefan
2 Fuhs, Carsten
2 Giesl, Jürgen
2 Hofmann, Martin
2 Jagannathan, Suresh
2 Katz, Ricardo David
2 Laporte, Vincent
2 Larsen, Kim Skak
2 Léchenet, Jean-Christophe
2 Leroy, Xavier
2 Marić, Filip
2 Nipkow, Tobias
2 Pesenti Gritti, Armando
2 Petri, Gustavo
2 Pilz, Alexander
2 Popescu, Andrei
2 Puebla, Germán
2 Raimondi, Franco
2 Steffen, Martin
2 Stolz, Volker
2 Stratulat, Sorin
2 Vitek, Jan
2 Zakowski, Yannick
1 Aderhold, Markus
1 Åman Pohjola, Johannes
1 Appel, Andrew W.
1 Arenas, Puri
1 Aschermann, Cornelius
1 Barbar, Mohamad
1 Barré, Nicolas
1 Bengtson, Jesper
1 Bernhard, David
1 Berthier, Nicolas
1 Betarte, Gustavo
1 Birkedal, Lars
1 Boender, Jaap P.
1 Boutry, Pierre
1 Brockschmidt, Marc
1 Brookes, Stephen D.
1 Brun, Christophe
1 Campo, Juan Diego
1 Cogumbreiro, Tiago
1 Cohen, Cyril
1 Dabrowski, Frédéric
1 Darais, David
1 Deng, Chaoqiang
1 Doczkal, Christian
1 Drămnesc, Isabela
1 Dupressoir, François
1 Fallah, Mehran S.
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 Jakobs, Marie-Christine
1 Jebelean, Tudor
1 Jensen, Thomas P.
1 Jones, Cliff B.
1 Kammüller, Florian
1 Kavanagh, Ryan
1 Khakpour, Narges
1 Kirchner, Florent
1 Kittelmann, Alexander
1 Komendantskaya, Ekaterina
1 Kosmatov, Nikolai
1 Lange, Julien
...and 51 more Authors

Citations by Year