David Cachera

According to our database, David Cachera authored at least 30 papers between 1995 and 2019.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2019

An ωω\omega-Algebra for Real-Time Energy Problems.

David Cachera, Uli Fahrenberg, Axel Legay

Log. Methods Comput. Sci., 2019

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology.

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

J. Autom. Reason., 2019

Combining Constraint Languages via Abstract Interpretation.

Pierre Talbot, David Cachera, Éric Monfroy, Charlotte Truchet

Proceedings of the 31st IEEE International Conference on Tools with Artificial Intelligence, 2019

2018

Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement.

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie

Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 2018

2017

An ω-Algebra for Real-Time Energy Problems.

David Cachera, Uli Fahrenberg, Axel Legay

CoRR, 2017

Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology.

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2016

An Extended Buffered Memory Model With Full Reorderings.

Gurvan Cabon, David Cachera, David Pichardie

Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, 2016

2015

An omega-Algebra for Real-Time Energy Problems.

David Cachera, Uli Fahrenberg, Axel Legay

Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

2014

Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases.

David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner

Sci. Comput. Program., 2014

2011

Programmation d'un interpréteur abstrait certifié en logique constructive.

David Cachera, David Pichardie

Tech. Sci. Informatiques, 2011

2010

Long-run cost analysis by approximation of linear operators over dioids.

David Cachera, Thomas P. Jensen, Arnaud Jobin, Pascal Sotin

Math. Struct. Comput. Sci., 2010

Injecting Abstract Interpretations into Linear Cost Models

David Cachera, Arnaud Jobin

Proceedings of the Proceedings Eighth Workshop on Quantitative Aspects of Programming Languages, 2010

A Certified Denotational Abstract Interpreter.

David Cachera, David Pichardie

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Comparing Techniques for Certified Static Analysis.

David Cachera, David Pichardie

Proceedings of the First NASA Formal Methods Symposium, 2009

Certified Static Analysis by Abstract Interpretation.

Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie

Proceedings of the Foundations of Security Analysis and Design V, 2009

2006

Quantitative Static Analysis Over Semirings: Analysing Cache Behaviour for Java Card.

Pascal Sotin, David Cachera, Thomas P. Jensen

Proceedings of the 4th International Workshop on Quantitative Aspects of Programming Languages, 2006

2005

Verification of safety properties for parameterized regular systems.

David Cachera, Katell Morin-Allory

ACM Trans. Embed. Comput. Syst., 2005

Extracting a data flow analyser in constructive logic.

David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu

Theor. Comput. Sci., 2005

Certified Memory Usage Analysis.

David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider

Proceedings of the FM 2005: Formal Methods, 2005

Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic.

Katell Morin-Allory, David Cachera

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2003

Embedding of Systems of Affine Recurrence Equations in Coq.

David Cachera, David Pichardie

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Verification of Control Properties in the Polyhedral Model.

David Cachera, Katell Morin-Allory

Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

2002

Advances in Bit Width Selection Methodology.

David Cachera, Tanguy Risset

Proceedings of the 13th IEEE International Conference on Application-Specific Systems, 2002

2001

Proving Properties of Multidimensional Recurrences with Application to Regular Parallel Algorithms.

David Cachera, Patrice Quinton, Sanjay V. Rajopadhye, Tanguy Risset

Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01), 2001

1998

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

David Cachera

PhD thesis, 1998

1997

Formal Validation of Data-Parallel Programs: A Two-Component Assertional Proof System for a Simple Language.

Luc Bougé, David Cachera, Yann Le Guyadec, Gil Utard, Bernard Virot

Theor. Comput. Sci., 1997

A logical framework to prove properties of Alpha programs.

Luc Bougé, David Cachera

Proceedings of the 1997 International Conference on Application-Specific Systems, 1997

1996

Proving Data-Parallel Programs: a Unifying Approach.

David Cachera, Gil Utard

Parallel Process. Lett., 1996

Formal Validation of Data Parallel Programs: Introducting the Assertional Approach.

Luc Bougé, David Cachera, Yann Le Guyadec, Gil Utard, Bernard Virot

Proceedings of the Data Parallel Programming Model: Foundations, 1996

1995

On the Completeness of a Proof System for a Simple Data-Parallel Programming Language.

Luc Bougé, David Cachera

Proceedings of the Euro-Par '95 Parallel Processing, 1995