Publications of David Cachera

Load the BibTeX file

Academic Journals

  1. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. Science of Computer Programming, To appear, 2014. download
  2. David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Mathematical Structures in Computer Science, 20(4):589-624, 2010.
  3. David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, 2005.
  4. David Cachera, Katell Morin-Allory. Verification of safety properties for parameterized regular systems. Trans. on Embedded Computing Systems, 4(2):228-266, 2005.

International Conferences

  1. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. In SAS - 19th International Static Analysis Symposium - 2012, Projet Région Bretagne CertLogs, Deauville, France, September 2012. download
  2. David Cachera, Arnaud Jobin. Injecting Abstract Interpretations into Linear Cost Models. In 8th Workshop on Quantitative Aspects of Programming Languages (QAPL), EPTCS, Paphos, 2010.
  3. David Cachera, David Pichardie. A Certified Denotational Abstract Interpreter. In Proc.\ of International Conference on Interactive Theorem Proving (ITP-10), Lecture Notes in Computer Science, Volume 6172, Pages 9-24, 2010.
  4. David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. In Proc.\ of the 1st NASA Formal Methods Symposium (NFM'09), Pages 111-115, 2009.
  5. David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. In Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Lectures Notes in Computer Science, Volume 5140, Pages 122-138, 2008.
  6. Pascal Sotin, David Cachera, Thomas Jensen. Quantitative Static Analysis over semirings: analysing cache behaviour for Java Card. In 4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006), Electronic Notes in Theoretical Computer Science, Volume 164, Pages 153-167, 2006.
  7. David Cachera, Thomas Jensen, David Pichardie, Gerardo Schneider. Certified Memory Usage Analysis. In Proc\. of 13th International Symposium on Formal Methods (FM'05), Lecture Notes in Computer Science, 2005.
  8. Katell Morin-Allory, David Cachera. Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic. In Proc. of 13th CHARME conference, Lecture Notes in Computer Science, Pages 376-379, 2005.
  9. David Cachera, Thomas Jensen, Pascal Sotin. Estimating Cache Misses with Semi-Modules and Quantitative Abstraction. In Proc. of IST-APPSEM II Workshop on Applied Semantics, 2005.
  10. David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. In Proc. ESOP'04, Springer LNCS, Pages 385-400, 2004.
  11. David Cachera, David Pichardie. Embedding of Systems of Affine Recurrence Equations in Coq. In Proc. TPHOLs 2003, 16th International Conference on Theorem Proving in Higher Order Logics , LNCS, Rome, Italy, September 2003. ps
  12. David Cachera, Katell Morin-Allory. Verification of Control Properties in the Polyhedral Model. In Proc. 1st MEMOCODE conference, Mont-St-Michel, France, June 2003. ps

Research Reports

  1. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Fast inference of polynomial invariants for imperative programs. Research Report INRIA, No 0, May 2011. download
  2. David Cachera, Thomas Jensen, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Research Report INRIA, No 6338, 2007. download
  3. David Cachera, Katell Morin-Allory. Proving Parameterized Systems: the use of a widening operator and pseudo-pipelines in polyhedral logic. Research Report TIMA-IMAG, No 0, 2005.
  4. David Cachera, Katell Morin-Allory. Verification of Control Properties in the Polyhedral Model. Research Report INRIA, No 1515, 2003. ps
  5. David Cachera, David Pichardie. Proof Tactics for the Verification of Structured Systems of Affine Recurrence Equations. Research Report INRIA, No 1511, 2003. ps

Misc

  1. Fré Besson, David Cachera, Thomas Jensen, David Pichardie. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. pp. 223-257, 2009.

Thesis

  1. David Cachera. Analyses statiques : certifier et quantifier. Habilitation ŕ diriger des recherches École normale supérieure de Cachan, 2010.