| 2015 | ICSE | Avoiding Security Pitfalls with Functional Programming: A Report on the Development of a Secure XML Validator. | Damien Doligez, Christle Faure, Thrse Hardin, Manuel Maarek |
| 2015 | LPAR | Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. | Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant |
| 2014 | CADE | Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. | Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz |
| 2013 | LPAR | Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. | David Delahaye, Damien Doligez, Frdric Gilbert, Pierre Halmagrand, Olivier Hermant |
| 2012 | FM | TLA + Proofs. | Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernn Vanzetto |
| 2012 | PLDI | Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the FoCaLiZe environment. | Damien Doligez, Mathieu Jaume, Renaud Rioboo |
| 2010 | CADE | Verifying Safety Properties with the TLA+ Proof System. | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2010 | ICTAC | The TLA | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2009 | POPL | A foundation for flow-based program matching: using temporal logic and model checking. | Julien Brunel, Damien Doligez, Ren Rydhof Hansen, Julia L. Lawall, Gilles Muller |
| 2008 | LPAR | A TLA+ Proof System. | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2007 | LPAR | Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. | Richard Bonichon, David Delahaye, Damien Doligez |
| 1999 | FM | Cache Coherence Verification with TLA+. | Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark R. Tuttle, Yuan Yu |
| 1994 | POPL | Portable, Unobtrusive Garbage Collection for Multiprocessor Systems. | Damien Doligez, Georges Gonthier |
| 1993 | POPL | A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML. | Damien Doligez, Xavier Leroy |