Research Themes

  • Formal Methods
  • Proof Assistants
  • Certified Static Analysis
  • Quantitative Aspects of Static Analysis
>>  the Celtique Team website

Selected Publications

  • Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, et al.. Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology. Proc. of ITP 2017, Brasília, Brazil, 2017
  • David Cachera, Ulrich Fahrenberg, Axel Legay An ω-Algebra for Real-Time Energy Problems. In Proc. of FSTTCS, Bengaluru, India, December 2015. [PDF]
  • David Cachera, Thomas P. Jensen, Arnaud Jobin and Florent Kirchner Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases. Science of Computer Programming, 93(B):89-109,2014.
  • David Cachera, Thomas Jensen, Arnaud Jobin and Pascal Sotin Long-run cost analysis by approximation of linear operators over dioids. Mathematical Structures in Computer Science, 20(4):589-624, 2010. [PDF]
  • David Cachera and David Pichardie. Proof Pearl: A Certified Denotational Abstract Interpreter. In Proc. of ITP'10, Edinburgh, Scottland, 2010. [PDF]

Students