Travelled to:1 × Estonia
1 × Italy
1 × USA
2 × United Kingdom
Collaborated with:D.Pichardie Y.F.d.Retana D.Sands L.Stefanesco G.Barthe V.Laporte L.Zhao S.Jagannathan J.Vitek A.A.d.Amorim N.Collins A.DeHon C.Hritcu B.C.Pierce R.Pollack A.Tolmach
Talks about:verifi (4) ssa (3) base (2) architectur (1) destruct (1) convent (1) coalesc (1) static (1) semant (1) secret (1)
Person: Delphine Demange
DBLP: Demange:Delphine
Contributed to:
2015
20142013
2012200920162018Wrote 7 papers:
- CC-2015-DemangePS #coq #optimisation #performance #verification
- Verifying Fast and Sparse SSA-Based Optimizations in Coq (DD, DP, LS), pp. 233–252.
- 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.
- ESOP-2012-BartheDP
- A Formally Verified SSA-Based Middle-End — Static Single Assignment Meets CompCert (GB, DD, DP), pp. 47–66.
- ESOP-2009-DemangeS
- All Secrets Great and Small (DD, DS), pp. 207–221.
- CC-2016-DemangeR
- Mechanizing conventional SSA for a verified destruction with coalescing (DD, YFdR), pp. 77–87.
- CC-2018-DemangeRP #reasoning #semantics
- Semantic reasoning about the sea of nodes (DD, YFdR, DP), pp. 163–173.