David Cachera

33 papers A 2B 5C 1Misc 1Journal 10Unranked 13
YearRankTypeTitle / Venue / Authors
2019 J jnl
An ωω\omega-Algebra for Real-Time Energy Problems.
Log. Methods Comput. Sci.
David Cachera, Uli Fahrenberg, Axel Legay
2019 B conf
Combining Constraint Languages via Abstract Interpretation.
ICTAI
Pierre Talbot, David Cachera, Éric Monfroy, Charlotte Truchet
2019 J jnl
Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology.
J. Autom. Reason.
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
2018 Misc conf
Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement.
SAC
Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie
2017 J jnl
An ω-Algebra for Real-Time Energy Problems.
CoRR
David Cachera, Uli Fahrenberg, Axel Legay
2017 B conf
Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology.
ITP
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
2016 — conf
An Extended Buffered Memory Model With Full Reorderings.
FTfJP@ECOOP
Gurvan Cabon, David Cachera, David Pichardie
2015 — conf
An omega-Algebra for Real-Time Energy Problems.
FSTTCS
David Cachera, Uli Fahrenberg, Axel Legay
2014 J jnl
Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases.
Sci. Comput. Program.
David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner
2012 B conf
Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases.
SAS
David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner
2011 J jnl
Programmation d'un interpréteur abstrait certifié en logique constructive.
Tech. Sci. Informatiques
David Cachera, David Pichardie
2010 B conf
A Certified Denotational Abstract Interpreter.
ITP
David Cachera, David Pichardie
2010 — conf
Injecting Abstract Interpretations into Linear Cost Models
QAPL
David Cachera, Arnaud Jobin
2010 J jnl
Long-run cost analysis by approximation of linear operators over dioids.
Math. Struct. Comput. Sci.
David Cachera, Thomas P. Jensen, Arnaud Jobin, Pascal Sotin
2009 — conf
Certified Static Analysis by Abstract Interpretation.
FOSAD
Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie
2009 — conf
Comparing Techniques for Certified Static Analysis.
NASA Formal Methods
David Cachera, David Pichardie
2008 — conf
Long-Run Cost Analysis by Approximation of Linear Operators over Dioids.
AMAST
David Cachera, Thomas P. Jensen, Arnaud Jobin, Pascal Sotin
2006 — conf
Quantitative Static Analysis Over Semirings: Analysing Cache Behaviour for Java Card.
QAPL
Pascal Sotin, David Cachera, Thomas P. Jensen
2005 B conf
Certified Memory Usage Analysis.
FM
David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider
2005 J jnl
Extracting a data flow analyser in constructive logic.
Theor. Comput. Sci.
David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
2005 — conf
Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic.
CHARME
Katell Morin-Allory, David Cachera
2005 J jnl
Verification of safety properties for parameterized regular systems.
ACM Trans. Embed. Comput. Syst.
David Cachera, Katell Morin-Allory
2004 A conf
Extracting a Data Flow Analyser in Constructive Logic.
ESOP
David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
2003 — conf
Embedding of Systems of Affine Recurrence Equations in Coq.
TPHOLs
David Cachera, David Pichardie
2003 C conf
Verification of Control Properties in the Polyhedral Model.
MEMOCODE
David Cachera, Katell Morin-Allory
2002 — conf
Advances in Bit Width Selection Methodology.
ASAP
David Cachera, Tanguy Risset
2001 A conf
Proving Properties of Multidimensional Recurrences with Application to Regular Parallel Algorithms.
IPDPS
David Cachera, Patrice Quinton, Sanjay V. Rajopadhye, Tanguy Risset
1998 — —
Validation formelle des langages à parallélisme de données. (Formal Validation of Data-Parallel Languages).
David Cachera
1997 — conf
A logical framework to prove properties of Alpha programs.
ASAP
Luc Bougé, David Cachera
1997 J jnl
Formal Validation of Data-Parallel Programs: A Two-Component Assertional Proof System for a Simple Language.
Theor. Comput. Sci.
Luc Bougé, David Cachera, Yann Le Guyadec, Gil Utard, Bernard Virot
1996 — conf
Formal Validation of Data Parallel Programs: Introducting the Assertional Approach.
The Data Parallel Programming Model
Luc Bougé, David Cachera, Yann Le Guyadec, Gil Utard, Bernard Virot
1996 J jnl
Proving Data-Parallel Programs: a Unifying Approach.
Parallel Process. Lett.
David Cachera, Gil Utard
1995 — conf
On the Completeness of a Proof System for a Simple Data-Parallel Programming Language.
Euro-Par
Luc Bougé, David Cachera