Computer Laboratory

Cristina David

Royal Society Research Fellow

Contact info

Department of Computer Science and Technology

University of Cambridge

J.J. Thomson Avenue

Cambridge CB3 0FD, England.

Office FC10

Research interests

Program synthesis, software verification, especially the verification of heap-manipulating programs, program termination and the design of decision procedures.

Selected publications

Counterexample Guided Inductive Synthesis Modulo Theories, Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Computer Aided Verification (CAV), 2018

Using Program Synthesis for Program Analysis, Cristina David, Daniel Kroening, Matt Lewis, ACM Transactions on Programming Languages and Systems (TOPLAS), 2018

Bit-Precise Procedure-Modular Termination Analysis, Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter, ACM Transactions on Programming Languages and Systems (TOPLAS), 2018

Program Synthesis: Challenges and Opportunities, Cristina David, Daniel Kroening, Philosophical Transactions A of the Royal Society, 2017

DSSynth: An Automated Digital Controller Synthesis Tool for Physical Plants, Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Automated Software Engineering (ASE), 2017

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants, Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Computer Aided Verification (CAV), 2017

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants, Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Hybrid Systems: Computation and Control (HSCC), 2017

Danger Invariants, Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis, Formal Methods (FM), 2016

Using Program Synthesis for Program Analysis, Cristina David, Daniel Kroening, Matt Lewis, Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), 2015

Synthesising Interprocedural Bit-Precise Termination Proofs, Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Bj\"{o}rn Wachter, Automated Software Engineering (ASE), 2015

Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs, Cristina David, Daniel Kroening, Matt Lewis, European Symposium on Programming (ESOP), 2015

Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs, Cristina David, Daniel Kroening, Matt Lewis, European Symposium on Programming (ESOP), 2015

Automatically inferring loop invariants via algorithmic learning, Yungbum Jung, Soonho Kong, Cristina David, Bow-Yaw Wang, Kwangkeun Yi, Mathematical Structures in Computer Science 25(4), 2015

Model and Proof Generation for Heap-Manipulating Programs, Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel, European Symposium on Programming (ESOP), 2014

HIPimm: verifying granular immutability guarantees, Andreea Costea, Asankhaya Sharma, Cristina David, Partial Evaluation and Semantics-based Program Manipulation (PEPM), 2014

Expressive program verification via structured specifications, Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin, Software Tools for Technology Transfer 16(4), 2014

Automated Verification of Shape, Size and Bag Properties via User-Defined Predicates in Separation Logic, Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin, Science of Computer Programming (SCP), 2012

Immutable Specifications for More Concise and Precise Verification, Cristina David, Wei-Ngan Chin, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2011

Structured Specifications for Better Verification of Heap-Manipulating Programs, Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin, International Conference on Formal Methods (FM), 2011

Enhancing Modular OO Verification with Separation Logic, Wei-Ngan Chin, Cristina David, Huu Hai Nguyen and Shengchao Qin, Principles of Programming Languages (POPL), 2008

Here is my DBLP publication list and here is my Google Scholar page.

Recent professional service

I've been on the program committee of Computer Aided Verification (CAV) 2018, Verified Software: Theories, Tools, and Experiments (VSTTE) 2018, Asian Symposium on Programming Languages and Systems (APLAS) 2018, Symposium on Applied Computing (SAC) 2019, Computer Aided Verification (CAV) 2019. I will serve on the committee of SYNT 2019.

I am also an associate editor for IET Software.

Until December 2021, I am on the Royal Society International Exchanges Panel.

Recent talks

Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants, SYNT@FLOC 2018

Should I join a startup?, invited talk at the Verification and Deductions Mentoring Workshop@FLOC 2018

Using Program Synthesis for Program Analysis, Imperial College London, December 2017

Solving Second-Order Constraints with Program Synthesis, City, University of London, October 2017

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants, Computer Aided Verification (CAV), 2017