Cristina David

Cristina David

Lecturer and Royal Society University Research Fellow

University of Bristol

Research Interests

Programming languages

Program synthesis

Program verification (especially of programs handling dynamically allocated data structures)

Design of decision procedures

Professional Service

I'll be on the program committee of CAV 2021 and ESOP 2022.

I am also an associate editor for IET Software and a member of the Royal Society International Exchanges Panel.

I was on the program committee of Computer Aided Verification (CAV) 2018-2020, Asian Symposium on Programming Languages and Systems (APLAS) 2018 and 2020, SYNT 2019, Symposium on Applied Computing (SAC-SVT) 2019-2021, Verified Software: Theories, Tools, and Experiments (VSTTE) 2018, Partial Evaluation and Program Manipulation (PEPM) 2012.

PhD Students

Joseph Bond (2020 --)

Yoav Alon (2020 --)

Pascal Kesseli (graduated in 2017) co-supervised with Daniel Kroening at University of Oxford

Selected Publications

Automated formal synthesis of provably safe digital controllers for continuous plants, Alessandro Abate, Iury Bessa, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Acta Informatica, 2020

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

Recent Talks

Program synthesis, Facebook Testing and Verification Symposium, November 2019

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