Programming languages
Program synthesis
Program verification (especially of programs handling dynamically allocated data structures)
Design of decision procedures
Programming languages
Program synthesis
Program verification (especially of programs handling dynamically allocated data structures)
Design of decision procedures
[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 am looking for motivated PhD students and postdoctoral researchers. Please get in touch if you are interested..
I'll be on the program committee of ICSE 2023, PEPM 2023 and SAC-SVT 2023.
I am 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-2021, European Symposium on Programming (ESOP) 2022, SYNT 2022, 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.
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
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
Program synthesis and applications to cyber-physical ystems, Workshop on Automata and Cyber-Physical Systems, Warwick, UK, April 2020
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