Travelled to:1 × Estonia
1 × Germany
1 × India
1 × Italy
1 × Japan
1 × Portugal
1 × South Africa
1 × Spain
2 × USA
3 × United Kingdom
Collaborated with:G.Barthe D.Demange V.Laporte T.P.Jensen S.Blazy V.Rusu D.Cachera S.Jagannathan J.Vitek L.Stefanesco F.Kirchner T.Rezk Y.F.d.Retana A.Maroneze C.Kunz J.Samborski-Forlese J.Forest G.Schneider J.Jourdan X.Leroy G.Petri L.Zhao B.Grégoire Rémi Hutin Alix Trieu A.A.d.Amorim N.Collins A.DeHon C.Hritcu B.C.Pierce R.Pollack A.Tolmach
Talks about:verifi (6) formal (4) static (3) verif (3) base (3) preserv (2) certifi (2) analysi (2) reason (2) memori (2)
Person: David Pichardie
DBLP: Pichardie:David
Contributed to:
2015
2015
201420142013
2013
20122011
20082007
2006
2005200420182020Wrote 15 papers:
- CC-2015-DemangePS #coq #optimisation #performance #verification
- Verifying Fast and Sparse SSA-Based Optimizations in Coq (DD, DP, LS), pp. 233–252.
- POPL-2015-JourdanLBLP #c
- A Formally-Verified C Static Analyzer (JHJ, VL, SB, XL, DP), pp. 247–259.
- PLDI-2014-JagannathanPVPL #compilation #refinement
- Atomicity refinement for verified compilation (SJ, GP, JV, DP, VL), p. 5.
- POPL-2014-AmorimCDDHPPPT #architecture #data flow
- A verified information-flow architecture (AAdA, NC, AD, DD, CH, DP, BCP, RP, AT), pp. 165–178.
- POPL-2013-DemangeLZJPV #java #memory management
- Plan B: a buffered memory model for Java (DD, VL, LZ, SJ, DP, JV), pp. 329–342.
- SAS-2013-BlazyLMP #abstract interpretation #analysis #c #verification
- Formal Verification of a C Value Analysis Based on Abstract Interpretation (SB, VL, AM, DP), pp. 324–344.
- ESOP-2012-BartheDP
- A Formally Verified SSA-Based Middle-End — Static Single Assignment Meets CompCert (GB, DD, DP), pp. 47–66.
- ESOP-2011-JensenKP #policy
- Secure the Clones — Static Enforcement of Policies for Secure Object Copying (TPJ, FK, DP), pp. 317–337.
- SEFM-2008-BartheKPS #hybrid #proving #verification
- Preservation of Proof Pbligations for Hybrid Verification Methods (GB, CK, DP, JSF), pp. 127–136.
- ESOP-2007-BarthePR #bytecode #java #lightweight #verification
- A Certified Lightweight Non-interference Java Bytecode Verifier (GB, DP, TR), pp. 125–140.
- FLOPS-2006-BartheFPR #coq #proving #reasoning #recursion
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant (GB, JF, DP, VR), pp. 114–129.
- FM-2005-CacheraJPS #analysis #memory management
- Certified Memory Usage Analysis (DC, TPJ, DP, GS), pp. 91–106.
- ESOP-2004-CacheraJPR #data flow #logic
- Extracting a Data Flow Analyser in Constructive Logic (DC, TPJ, DP, VR), pp. 385–400.
- CC-2018-DemangeRP #reasoning #semantics
- Semantic reasoning about the sea of nodes (DD, YFdR, DP), pp. 163–173.
- POPL-2020-BartheBGHLPT #c #compilation #verification
- Formal verification of a constant-time preserving C compiler (GB, SB, BG, RH, VL, DP, AT), p. 30.