| [1] |
David Cachera and David Pichardie.
Programmation d'un interpréteur abstrait certifié en logique
constructive.
Technique et Science Informatiques (TSI), 2010.
To appear. [ bib ] |
| [2] |
Frédéric Besson, Thomas Jensen, Guillaume Dufay, and David Pichardie.
Verifying resource access control on mobile interactive devices.
Journal of Computer Security, 2010.
To appear. [ bib | .pdf ] |
| [3] |
Frédéric Besson, David Cachera, Thomas P. Jensen, and David Pichardie.
In Foundations of Security Analysis and Design V, FOSAD
2007/2008/2009 Tutorial Lectures, volume 5705 of Lecture Notes in
Computer Science, pages 223-257. Springer-Verlag, 2009. [ bib | .pdf ] |
| [4] |
Frédéric Dabrowski and David Pichardie.
A certified data race analysis for a java-like language.
In Proc. of 22nd International Conference on Theorem Proving in
Higher Order Logics (TPHOLs'09), volume 5674 of Lecture Notes in
Computer Science, pages 212-227. Springer-Verlag, 2009. [ bib | .pdf ] |
| [5] |
David Cachera and David Pichardie.
Comparing techniques for certified static analysis.
Proc. of the 1st NASA Formal Methods Symposium (NFM'09), pages
111-115, 2009. [ bib | .pdf ] |
| [6] |
Laurent Hubert and David Pichardie.
Soundly handling static fields: Issues, semantics and analysis.
Proc. of the 4th International Workshop on Bytecode Semantics,
Verification, Analysis and Transformation (BYTECODE'09), 2009.
To appear. [ bib | .pdf ] |
| [7] |
Gilles Barthe, César Kunz, David Pichardie, and Julián Samborski Forlese.
Preservation of proof obligations for hybrid certificates.
In Proc. of the 6th IEEE International Conferences on Software
Engineering and Formal Methods (SEFM'08). IEEE Computer Society, 2008.
To appear. [ bib | .pdf ] |
| [8] |
Laurent Hubert, Thomas Jensen, and David Pichardie.
Semantic foundations and inference of non-null annotations.
In Proc. of the 10th International Conference on Formal Methods
for Open Object-based Distributed Systems (FMOODS'08), volume 5051 of
Lecture Notes in Computer Science, pages 132-149. Springer-Verlag, 2008. [ bib | .pdf ] |
| [9] |
David Pichardie.
Building certified static analysers by modular construction of
well-founded lattices.
In Proc. of the 1st International Conference on Foundations of
Informatics, Computing and Software (FICS'08), volume 212 of Electronic
Notes in Theoretical Computer Science, pages 225-239, 2008. [ bib | .pdf ] |
| [10] |
Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, and David
Pichardie.
The MOBIUS Proof Carrying Code infrastructure.
In Proc. of the 6th International Symposium on Formal Methods
for Components and Objects (FMCO'07), Lecture Notes in Computer Science.
Springer-Verlag, 2007.
To appear. [ bib ] |
| [11] |
Gilles Barthe, David Pichardie, and Tamara Rezk.
A Certified Lightweight Non-Interference Java Bytecode Verifier.
In Proc. of 16th European Symposium on Programming (ESOP'07),
volume 4421 of Lecture Notes in Computer Science, pages 125-140.
Springer-Verlag, 2007. [ bib | .pdf ] |
| [12] |
Frédéric Besson, Thomas Jensen, and David Pichardie.
Proof-carrying code from certified abstract interpretation to
fixpoint compression.
Theoretical Computer Science, 364(3):273-291, 2006. [ bib | .pdf ] |
| [13] |
Frédéric Besson, Thomas Jensen, and David Pichardie.
A PCC Architecture based on Certified Abstract Interpretation.
In Proc. of 1st International Workshop on Emerging Applications
of Abstract Interpretation (EAAI'06), ENTCS. Springer-Verlag, 2006. [ bib | .pdf ] |
| [14] |
Gilles Barthe, Julien Forest, David Pichardie, and Vlad Rusu.
Defining and reasoning about recursive functions: A practical tool
for the coq proof assistant.
In Proc of 8th International Symposium on Functional and Logic
Programming (FLOPS'06), volume 3945 of Lecture Notes in Computer
Science, pages 114-129. Springer-Verlag, 2006. [ bib | .pdf ] |
| [15] |
Pichardie David.
Interprétation abstraite en logique intuitionniste : extraction
d'analyseurs Java certifiés.
PhD thesis, Université Rennes 1, 2005.
In french. [ bib | .pdf ] |
| [16] |
David Pichardie.
Modular proof principles for parameterized concretizations.
In Proc. of 2nd International Workshop on Construction and
Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2005),
number 3956 in Lecture Notes in Computer Science, pages 138-154.
Springer-Verlag, 2005. [ bib | .pdf ] |
| [17] |
David Cachera, Thomas Jensen, David Pichardie, and Gerardo Schneider.
Certified Memory Usage Analysis.
In Proc of 13th International Symposium on Formal Methods
(FM'05), number 3582 in Lecture Notes in Computer Science, pages 91-106.
Springer-Verlag, 2005. [ bib | .pdf ] |
| [18] |
David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu.
Extracting a Data Flow Analyser in Constructive Logic.
Theoretical Computer Science, 342(1):56-78, September 2005.
Extended version of [19]. [ bib | .pdf ] |
| [19] |
David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu.
Extracting a Data Flow Analyser in Constructive Logic.
In Proc. of 13th European Symposium on Programming (ESOP'04),
number 2986 in Lecture Notes in Computer Science, pages 385-400.
Springer-Verlag, 2004. [ bib | .pdf ] |
| [20] |
Thomas Genet, Thomas Jensen, Vikash Kodati, and David Pichardie.
A Java Card CAP converter in PVS.
In Jens Knoop and Wolf Zimmermann, editors, Proc. of 2nd
International Workshop on Compiler Optimization Meets Compiler Verification
(COCV 2003), Electronic Notes in Theoretical Computer Science, volume 82.
Elsevier, 2004. [ bib | .pdf ] |
| [21] |
David Cachera and David Pichardie.
Embedding of Systems of Affine Recurrence Equations in Coq.
In Proc. of 16th International Conference on Theorem Proving in
Higher Order Logics (TPHOLs'03), number 2758 in Lecture Notes in Computer
Science, pages 155-170. Springer-Verlag, 2003. [ bib | .pdf ] |
| [22] |
David Pichardie and Yves Bertot.
Formalizing Convex Hulls Algorithms.
In Proc. of 14th International Conference on Theorem Proving in
Higher Order Logics (TPHOLs'01), number 2152 in Lecture Notes in Computer
Science, pages 346-361. Springer-Verlag, 2001. [ bib | .pdf ] |
This file has been generated by bibtex2html 1.73