| 2019 | ICTAI | Combining Constraint Languages via Abstract Interpretation. | Pierre Talbot, David Cachera, ric Monfroy, Charlotte Truchet |
| 2018 | SAC | Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement. | Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie |
| 2017 | ITP | Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. | Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek |
| 2016 | ECOOP | An Extended Buffered Memory Model With Full Reorderings. | Gurvan Cabon, David Cachera, David Pichardie |
| 2012 | SAS | Inference of Polynomial Invariants for Imperative Programs: A Farewell to Grbner Bases. | David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner |
| 2010 | ITP | A Certified Denotational Abstract Interpreter. | David Cachera, David Pichardie |
| 2005 | FM | Certified Memory Usage Analysis. | David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider |
| 2004 | ESOP | Extracting a Data Flow Analyser in Constructive Logic. | David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu |
| 2003 | MEMOCODE | Verification of Control Properties in the Polyhedral Model. | David Cachera, Katell Morin-Allory |
| 1995 | EuroPar | On the Completeness of a Proof System for a Simple Data-Parallel Programming Language. | Luc Boug, David Cachera |