Travelled to:
1 × USA
1 × United Kingdom
Collaborated with:
Z.Shao J.Hoffmann J.H.0002 V.C.Ngo T.Ramananandro T.W.Reps
Talks about:
resourc (3) bound (3) program (2) analysi (2) end (2) probabilist (1) composit (1) certifi (1) object (1) expect (1)
Person: Quentin Carbonneaux
DBLP: Carbonneaux:Quentin
Contributed to:
Wrote 4 papers:
- PLDI-2015-Carbonneaux0S #bound #composition
- Compositional certified resource bounds (QC, JH, ZS), pp. 467–478.
- PLDI-2014-Carbonneaux0RS #bound #c #source code #verification
- End-to-end verification of stack-space bounds for C programs (QC, JH, TR, ZS), p. 30.
- CAV-2017-Carbonneaux0RS #analysis #automation #coq #proving
- Automated Resource Analysis with Coq Proof Objects (QC, JH0, TWR, ZS), pp. 64–85.
- PLDI-2018-NgoC0 #analysis #bound #probability #source code
- Bounded expectations: resource analysis for probabilistic programs (VCN, QC, JH0), pp. 496–512.