Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. “A Formally-Verified C Static Analyzer.” In Proc. of the 42th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. ACM, 2015. pdf.
Sandrine Blazy, Vincent Laporte, and David Pichardie. “Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code.” In Proc. of the 5th conference on Interactive Theorem Proving (ITP). Lecture Notes in Computer Science. Springer-Verlag, 2014. pdf.
Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, and Jan Vitek. “Atomicity Refinement for Verified Compilation.” ACM Transactions on Programming Languages and Systems (TOPLAS) (to be published). pdf.
Sandrine Blazy, Vincent Laporte, André Maroneze, and David Pichardie. “Formal Verification of a C Value Analysis Based on Abstract Interpretation.” In Proc. of the 20th Static Analysis Symposium (SAS 2013). Lecture Notes in Computer Science. Springer-Verlag, 2013. pdf.
Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, and Jan Vitek. “Plan B: A Buffered Memory Model for Java.” In Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013. ACM, 2013. pdf.
Gilles Barthe, Marion Daubignard, Bruce Kapron, Yassine Lakhnech, and Vincent Laporte. “On the equality of probabilistic terms.” In Logic for Programming, Artificial Intelligence, and Reasoning, 46–63. Springer, 2010. pdf.