David Cachera

According to our database1, David Cachera authored at least 30 papers between 1995 and 2018.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.



In proceedings 
PhD thesis 


On csauthors.net:


Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement.
Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 2018

An ω-Algebra for Real-Time Energy Problems.
CoRR, 2017

Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

An Extended Buffered Memory Model With Full Reorderings.
Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, 2016

An omega-Algebra for Real-Time Energy Problems.
Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases.
Sci. Comput. Program., 2014

Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases.
Proceedings of the Static Analysis - 19th International Symposium, 2012

Programmation d'un interpréteur abstrait certifié en logique constructive.
Technique et Science Informatiques, 2011

Long-run cost analysis by approximation of linear operators over dioids.
Mathematical Structures in Computer Science, 2010

Injecting Abstract Interpretations into Linear Cost Models
Proceedings of the Proceedings Eighth Workshop on Quantitative Aspects of Programming Languages, 2010

A Certified Denotational Abstract Interpreter.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Comparing Techniques for Certified Static Analysis.
Proceedings of the First NASA Formal Methods Symposium, 2009

Certified Static Analysis by Abstract Interpretation.
Proceedings of the Foundations of Security Analysis and Design V, 2009

Long-Run Cost Analysis by Approximation of Linear Operators over Dioids.
Proceedings of the Algebraic Methodology and Software Technology, 2008

Quantitative Static Analysis Over Semirings: Analysing Cache Behaviour for Java Card.
Electr. Notes Theor. Comput. Sci., 2006

Verification of safety properties for parameterized regular systems.
ACM Trans. Embedded Comput. Syst., 2005

Extracting a data flow analyser in constructive logic.
Theor. Comput. Sci., 2005

Certified Memory Usage Analysis.
Proceedings of the FM 2005: Formal Methods, 2005

Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic.
Proceedings of the Correct Hardware Design and Verification Methods, 2005

Extracting a Data Flow Analyser in Constructive Logic.
Proceedings of the Programming Languages and Systems, 2004

Embedding of Systems of Affine Recurrence Equations in Coq.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Verification of Control Properties in the Polyhedral Model.
Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

Advances in Bit Width Selection Methodology.
Proceedings of the 13th IEEE International Conference on Application-Specific Systems, 2002

Proving Properties of Multidimensional Recurrences with Application to Regular Parallel Algorithms.
Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01), 2001

Validation formelle des langages à parallélisme de données. (Formal Validation of Data-Parallel Languages).
PhD thesis, 1998

Formal Validation of Data-Parallel Programs: A Two-Component Assertional Proof System for a Simple Language.
Theor. Comput. Sci., 1997

A logical framework to prove properties of Alpha programs.
Proceedings of the 1997 International Conference on Application-Specific Systems, 1997

Proving Data-Parallel Programs: a Unifying Approach.
Parallel Processing Letters, 1996

Formal Validation of Data Parallel Programs: Introducting the Assertional Approach.
Proceedings of the Data Parallel Programming Model: Foundations, 1996

On the Completeness of a Proof System for a Simple Data-Parallel Programming Language.
Proceedings of the Euro-Par '95 Parallel Processing, 1995