Publications

[BDP12] A formally verified ssa-based middle-end - Static Single Assignment meets CompCert. G. Barthe, D. Demange, and D. Pichardie. In Proc. of 21th European Symposium on Programming (ESOP 2012), Lecture Notes in Computer Science. Springer-Verlag, 2012. To appear.
[DJP10] A provably correct stackless intermediate representation for Java bytecode. D. Demange, T. Jensen, and D. Pichardie. In Proc. of the 8th Asian Symposium on Programming Languages and Systems (APLAS 2010), volume 6461 of Lecture Notes in Computer Science, pages 97-113. Springer-Verlag, 2010. [.pdf]
[HBBD10] Sawja: Static Analysis Workshop for Java. L. Hubert, N. Barré, F. Besson, D. Demange, T. Jensen, V. Monfort, D. Pichardie, and T. Turpin. In Proc. of the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), volume 6528 of Lecture Notes in Computer Science, pages 82-106. Springer-Verlag, 2011. [.pdf]
[DS09a] All Secrets Great and Small. D. Demange and D. Sands. In Programming Languages and Systems. 18th European Symposium on Programming, ESOP 2009, number 5502 in LNCS. Springer Verlag, 2009. [.pdf]

Technical and Research reports

[BDP11] A formally veriﬁed SSA-based middle-end compiler. G. Barthe, D. Demange and D. Pichardie. Research Report 634702, INRIA, 2011. [.pdf]
[DJP09] A Provably Stackless Intermediate Representation for Java Bytecode. D. Demange and T. Jensen and D. Pichardie. Research Report 7021, INRIA, 2009. Extended version of [DJP10][.pdf]
[DS09b] All Secrets Great and Small. D. Demange and D. Sands. Technical report, Chalmers University of Technology and Goteborgs University, March 2009. Extended version of [DS09a]. [.pdf]

Formal proof of Randomized Algorithms - Advisor: Philippe Audebaud - Undergratuate Internship (2007) at LIP - ENS Lyon (PLUME team) [.pdf]