G. Barthe, M. Pavlova, and G. Schneider.
Precise analysis of memory consumption using program logics.
In B. Aichernig and B. Beckert, editors, Proceedings of
SEFM'05, pages 86-95, Koblenz, Germany, September 2005. IEEE Computer
Society.
[ bib |
.pdf ]
D. Gurov and M. Huisman.
Interface abstraction for compositional verification.
In B. Aichernig and B. Beckert, editors, Proceedings of
SEFM'05, pages 414-423, Koblenz, Germany, September 2005. IEEE Computer
Society.
An earlier version appeared as INRIA Technical Report, nr. RR-5330.
[ bib |
.ps.gz ]
B. Grégoire and A. Mahboubi.
Proving equalities in a commutative ring done right in Coq.
In J. Hurd and T. Melham, editors, Proceedings of TPHOLs'05,
volume 3603 of Lecture Notes in Computer Science, pages 98-113,
Oxford, UK, August 2005. Springer-Verlag.
[ bib |
.ps.gz ]
B. Barras and B. Grégoire.
On the role of type decorations in the calculus of inductive
constructions.
In L. Ong, editor, Proceedings of CSL'05, volume 3634 of Lecture Notes in Computer Science, pages 151-166, Oxford, UK, August 2005.
Springer-Verlag.
[ bib |
.ps.gz ]
G. Barthe, B. Grégoire, and F. Pastawski.
Practical inference for typed-based termination in a polymorphic
setting.
In P. Urzyczyn, editor, Proceedings of TLCA'05, volume 3641
of Lecture Notes in Computer Science, pages 71-85, Nara, Japan, April
2005. Springer-Verlag.
[ bib |
.ps.gz ]
M. Huisman and K. Trentelman.
Factorising temporal specifications.
In M. Atkinson and F. Dehne, editors, Proceedings of CATS'05,
volume 41 of Conferences in Research and Practice in Information
Technology, pages 87-96, Newcastle, Australia, February 2005. ACSC.
An earlier version appeared as INRIA Technical Report, nr. RR-5326.
[ bib |
.ps.gz ]
S. Zanella Béguelin.
Formalisation and verification of the GlobalPlatform Card
Specification using the B method.
In G. Barthe, B. Grégoire, M. Huisman, and J.-L. Lanet, editors,
Construction and Analysis of Safe, Secure, and Interoperable Smart
Devices, Second International Workshop, CASSIS 2005, Nice, France, March
8-11 2005, volume 3956 of Lecture Notes in Computer Science, pages
155-173. Springer-Verlag, 2005.
[ bib |
http ]
G. Barthe, T. Rezk, and A. Saabas.
Proof obligations preserving compilation.
In R. Gorrieri, F. Martinelli, P. Ryan, and S. Schneider, editors,
Proceedings of FAST'05, volume 3866 of Lecture Notes in Computer
Science, pages 112-126. Springer-Verlag, 2005.
[ bib |
.pdf ]
S. Tarento.
Machine-checked security proofs of cryptographic signature schemes.
In S. De Capitani di Vimercati, P.F. Syverson, and D. Gollmann,
editors, Proceedings of ESORICS'05, volume 3679 of Lecture Notes
in Computer Science, pages 140-158. Springer-Verlag, 2005.
[ bib |
.pdf ]
G. Barthe, T. Rezk, and M. Warnier.
Preventing timing leaks through transactional branching instructions.
In Proceedings of 3rd Workshop on Quantitative Aspects of
Programming Languages (QAPL'05), Edinburgh, Scotland, 2005. Electronic Notes
in Theoretical Computer Science.
to appear.
[ bib |
.pdf ]
G. Barthe and T. Rezk.
Non-interference for a JVM-like language.
In M. Fähndrich, editor, Proceedings of TLDI'05, pages
103-112, Long Beach, USA, January 2005. ACM Press.
[ bib |
.ps.gz ]
Y. Bertot, B. Grégoire, and X. Leroy.
A structured approach to proving compiler optimizations based on
dataflow analysis.
In J.C. Filliâtre, C. Paulin-Mohring, and B. Werner, editors,
Proceedings of TYPES'04, volume 3839 of Lecture Notes in Computer
Science, pages 66 - 81. Springer-Verlag, 2005.
[ bib |
.ps.gz ]