Cristina David

Cristina David

Senior Lecturer (Associate Professor) and Royal Society University Research Fellow

University of Bristol

Research Interests

Programming languages

Code generation (both rule-based and LLM-based)

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

Design of decision procedures

Ongoing projects

C to Rust translation:

  Ownership Guided C to Rust Translation [pdf]

  Towards Translating Real-World Code with LLMs: A Study of Translating to Rust [preprint]

Synthesis of SQL queries:

   Enhancing SQL Query Generation with Neurosymbolic Reasoning [preprint]

Java refactoring:

   Quantifying the benefits of code hints for refactoring deprecated Java APIs [preprint]

Enhancing LLM's long-term planning with Reinforcement Learning:

   Integrating Large Language Models and Reinforcement Learning for Non-Linear Reasoning [preprint]



I am looking for motivated PhD students and postdoctoral researchers. Please get in touch if you are interested..

News

[Oct 2022] I'll be on the program committee of ICSE 2024 and CAV 2023. Also, I'll be PC co-chair of TASE 2023.

[Sept 2022] Invited talk at King's College on our FSE'22 paper Using Graph Neural Networks for Program Termination.

[May 2022] My Royal Society URF has been extended until 06/2026.

I'll be on the program committee of ICSE 2023, PEPM 2023 and SAC-SVT 2023.

PhD Students

Joseph Bond (2020 --)

Yoav Alon (2020 --)

Hanliang Zhang (2022 --) (second supervisor)

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

Selected Publications

Ownership guided C to Rust translation, Hanliang Zhang, Cristina David, Yijun Yu, Meng Wang, CAV, 2023

Synthesising Programs with Non-trivial Constants, Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli, J. Autom. Reason. 67(2): 19, 2023

Using Graph Neural Networks for Program Termination, Yoav Alon, Cristina David, FSE, 2022

Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches, Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang, OOPSLA, 2021

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