Travelled to:1 × Ireland
1 × United Kingdom
2 × France
4 × USA
Collaborated with:W.Chin D.Kröning S.Qin M.Lewis D.Kroening C.Gherghina H.H.Nguyen P.Schrammel A.Abate P.Kesseli E.Polgreen A.Costea A.Sharma M.Brain I.Bessa D.Cattaruzza L.C.Cordeiro H.Chen B.Wachter L.C.Chaves
Talks about:program (4) termin (4) verif (4) synthesi (3) manipul (3) autom (3) heap (3) control (2) specif (2) precis (2)
Person: Cristina David
DBLP: David:Cristina
Contributed to:
20152014
2014
2011
20112009
2008
2007
20152017
20172018Wrote 13 papers:
- ESOP-2015-DavidKL #source code #strict #termination
- Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs (CD, DK, ML), pp. 183–204.
- ESOP-2015-DavidKL15a #reasoning #safety #source code #termination
- Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs (CD, DK, ML), pp. 661–684.
- ESOP-2014-BrainDKS #generative #proving #source code
- Model and Proof Generation for Heap-Manipulating Programs (MB, CD, DK, PS), pp. 432–452.
- PEPM-2014-CosteaSD #named #verification
- HIPimm: verifying granular immutability guarantees (AC, AS, CD), pp. 189–194.
- FM-2011-GherghinaDQC #source code #specification #verification
- Structured Specifications for Better Verification of Heap-Manipulating Programs (CG, CD, SQ, WNC), pp. 386–401.
- OOPSLA-2011-DavidC #precise #specification #verification
- Immutable specifications for more concise and precise verification (CD, WNC), pp. 359–374.
- PEPM-2009-DavidGC #calculus #exception #optimisation
- Translation and optimization for a core calculus with exceptions (CD, CG, WNC), pp. 41–50.
- POPL-2008-ChinDNQ #composition #logic #object-oriented #verification
- Enhancing modular OO verification with separation logic (WNC, CD, HHN, SQ), pp. 87–99.
- VMCAI-2007-NguyenDQC #automation #logic #verification
- Automated Verification of Shape and Size Properties Via Separation Logic (HHN, CD, SQ, WNC), pp. 251–266.
- ASE-2015-ChenDKSW #interprocedural #proving #termination
- Synthesising Interprocedural Bit-Precise Termination Proofs (T) (HYC, CD, DK, PS, BW), pp. 53–64.
- ASE-2017-AbateBCCCDKKP #automation #named #physics #synthesis
- DSSynth: an automated digital controller synthesis tool for physical plants (AA, IB, DC, LCC, LCC, CD, PK, DK, EP), pp. 919–924.
- CAV-2017-AbateBCCDKKP #automation #physics #synthesis
- Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants (AA, IB, DC, LCC, CD, PK, DK, EP), pp. 462–482.
- CAV-2018-AbateDKKP #induction #modulo theories #synthesis
- Counterexample Guided Inductive Synthesis Modulo Theories (AA, CD, PK, DK, EP), pp. 270–288.