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

Publications by Year

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.68616
Barthe, Gilles; Forest, Julien; Pichardie, David; Rusu, Vlad
11
2006
Formalizing convex hull algorithms. Zbl 1005.68557
Pichardie, David; Bertot, Yves
9
2001
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
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
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
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.68098
Demange, Delphine; Laporte, Vincent; Zhao, Lei; Jagannathan, Suresh; Pichardie, David; Vitek, Jan
4
2013
Extracting a data flow analyser in constructive logic. Zbl 1126.68345
Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad
3
2004
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
3
2017
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
An abstract memory functor for verified C static analyzers. Zbl 1361.68058
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
2
2016
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
2
2020
Modular SMT proofs for fast reflexive checking inside Coq. Zbl 1350.68224
Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David
1
2011
Embedding of systems of affine recurrence equations in Coq. Zbl 1279.68286
Cachera, David; Pichardie, David
1
2003
Validating dominator trees for a fast, verified dominance test. Zbl 1466.68030
Blazy, Sandrine; Demange, Delphine; Pichardie, David
1
2015
A certified data race analysis for a Java-like language. Zbl 1252.68054
Dabrowski, Frédéric; Pichardie, David
1
2009
Secure the clones. Zbl 1238.68047
Jensen, Thomas; Kirchner, Florent; Pichardie, David
1
2012
Secure the clones. Static enforcement of policies for secure object copying. Zbl 1326.68098
Jensen, Thomas; Kirchner, Florent; Pichardie, David
1
2011
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
2
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
3
2017
An abstract memory functor for verified C static analyzers. Zbl 1361.68058
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
2
2016
Validating dominator trees for a fast, verified dominance test. Zbl 1466.68030
Blazy, Sandrine; Demange, Delphine; Pichardie, David
1
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
4
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
1
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
5
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
11
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
9
2001
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

Citations by Year