G. Barthe, B. Grégoire, C. Kunz, and T. Rezk.
Certificate translation for optimizing compilers.
In Proceedings of the 13th International Static Analysis
Symposium (SAS), LNCS, Seoul, Korea, August 2006. Springer-Verlag.
[ bib |
.pdf ]
G. Barthe, D. Naumann, and T. Rezk.
Deriving an information flow checker and certifying compiler for
Java.
In Proceedings of Symposium of Security and Privacy'06. IEEE
Press, 2006.
[ bib |
.ps ]
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 ]
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 ]
G. Barthe, P. D'Argenio, and T. Rezk.
Secure Information Flow by Self-Composition.
In R. Foccardi, editor, Proceedings of CSFW'04, pages 100-114,
Pacific Grove,USA, June 2004. IEEE Press.
[ bib |
.ps.gz ]