Παρακολούθηση
David Pichardie
David Pichardie
Professor, ENS Rennes, France
Η διεύθυνση ηλεκτρονικού ταχυδρομείου έχει επαληθευτεί στον τομέα inria.fr - Αρχική σελίδα
Τίτλος
Παρατίθεται από
Παρατίθεται από
Έτος
A formally-verified C static analyzer
JH Jourdan, V Laporte, S Blazy, X Leroy, D Pichardie
ACM SIGPLAN Notices 50 (1), 247-259, 2015
1912015
System-level non-interference for constant-time cryptography
G Barthe, G Betarte, J Campo, C Luna, D Pichardie
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications …, 2014
1382014
A certified lightweight non-interference java bytecode verifier
G Barthe, D Pichardie, T Rezk
European Symposium on Programming, 125-140, 2007
1142007
A verified information-flow architecture
A Azevedo de Amorim, N Collins, A DeHon, D Demange, C Hriţcu, ...
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014
1102014
Extracting a data flow analyser in constructive logic
D Cachera, T Jensen, D Pichardie, V Rusu
European Symposium on Programming, 385-400, 2004
1072004
A formally verified SSA-based middle-end
G Barthe, D Demange, D Pichardie
European Symposium on Programming, 47-66, 2012
80*2012
Proof-carrying code from certified abstract interpretation and fixpoint compression
F Besson, T Jensen, D Pichardie
Theoretical Computer Science 364 (3), 273-291, 2006
792006
Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant
G Barthe, J Forest, D Pichardie, V Rusu
International Symposium on Functional and Logic Programming, 114-129, 2006
732006
Formal verification of a constant-time preserving C compiler
G Barthe, S Blazy, B Grégoire, R Hutin, V Laporte, D Pichardie, A Trieu
Proceedings of the ACM on Programming Languages 4 (POPL), 1-30, 2020
692020
Semantic foundations and inference of non-null annotations
L Hubert, T Jensen, D Pichardie
International Conference on Formal Methods for Open Object-Based Distributed …, 2008
682008
Certified memory usage analysis
D Cachera, T Jensen, D Pichardie, G Schneider
International Symposium on Formal Methods, 91-106, 2005
622005
Formal verification of a C value analysis based on abstract interpretation
S Blazy, V Laporte, A Maroneze, D Pichardie
International Static Analysis Symposium, 324-344, 2013
542013
Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés
D Pichardie
PhD thesis, University Rennes 1, 2005
542005
Formalizing convex hull algorithms
D Pichardie, Y Bertot
International Conference on Theorem Proving in Higher Order Logics, 346-361, 2001
53*2001
Verifying constant-time implementations by abstract interpretation
S Blazy, D Pichardie, A Trieu
Journal of Computer Security 27 (1), 137-163, 2019
462019
Plan B: A buffered memory model for Java
D Demange, V Laporte, L Zhao, S Jagannathan, D Pichardie, J Vitek
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013
442013
The MOBIUS proof carrying code infrastructure
G Barthe, P Crégut, B Grégoire, T Jensen, D Pichardie
International Symposium on Formal Methods for Components and Objects, 1-24, 2007
442007
Sawja: Static analysis workshop for java
L Hubert, N Barré, F Besson, D Demange, T Jensen, V Monfort, ...
International Conference on Formal Verification of Object-Oriented Software …, 2010
432010
A certified denotational abstract interpreter
D Cachera, D Pichardie
International Conference on Interactive Theorem Proving, 9-24, 2010
422010
A certified lightweight non-interference java bytecode verifier
G Barthe, D Pichardie, T Rezk
Mathematical Structures in Computer Science 23 (5), 1032-1081, 2013
362013
Δεν είναι δυνατή η εκτέλεση της ενέργειας από το σύστημα αυτή τη στιγμή. Προσπαθήστε ξανά αργότερα.
Άρθρα 1–20