Travelled to:1 × India
Collaborated with:K.R.M.Leino B.Delaware J.Gross A.Chlipala G.Martínez D.Ahman V.Dumitrescu N.Giannarakis C.Hawblitzel C.Hritcu M.Narasimhamurthy Z.Paraskevopoulou J.Protzenko T.Ramananandro A.Rastogi N.Swamy
Talks about:proof (2) metaprogram (1) synthesi (1) strategi (1) abstract (1) trigger (1) program (1) verifi (1) tactic (1) stabil (1)
Person: Clément Pit-Claudel
DBLP: Pit-Claudel:Cl=eacute=ment
Contributed to:
2015
2019
2016Wrote 3 papers:
- POPL-2015-DelawarePGC #data type #deduction #named #proving #synthesis
- Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant (BD, CPC, JG, AC), pp. 689–700.
- ESOP-2019-MartinezADGHHNP #automation #metaprogramming #proving #smt
- Meta-F* : Proof Automation with SMT, Tactics, and Metaprograms (GM, DA, VD, NG, CH, CH, MN, ZP, CPC, JP, TR, AR, NS), pp. 30–59.
- CAV-2016-LeinoP #verification
- Trigger Selection Strategies to Stabilize Program Verifiers (KRML, CPC), pp. 361–381.