Multiple Pre/Post Specifications for Heap-Manipulating Methods. - Wei-Ngan Chin; Cristina David; Huu Hai Nguyen; Shengchao Qin (HASE, 2007)

Automated Verification of Shape, Size and Bag Properties. - Wei-Ngan Chin; Cristina David; Huu Hai Nguyen; Shengchao Qin (ICECCS, 2007)

Automated Verification of Shape and Size Properties Via Separation Logic. - Huu Hai Nguyen; Cristina David; Shengchao Qin; Wei-Ngan Chin (VMCAI, 2007)

Enhancing modular OO verification with separation logic. - Wei-Ngan Chin; Cristina David; Huu Hai Nguyen; Shengchao Qin (POPL, 2008)

Translation and optimization for a core calculus with exceptions. - Cristina David; Cristian Gherghina; Wei-Ngan Chin (PEPM, 2009)

Automated Verification Using Unified Control Flows. - Cristian Gherghina; Cristina David (TASE, 2009)

Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. - Soonho Kong; Yungbum Jung; Cristina David; Bow-Yaw Wang; Kwangkeun Yi (APLAS, 2010)

A Specification Logic for Exceptions and Beyond. - Cristian Gherghina; Cristina David (ATVA, 2010)

Structured Specifications for Better Verification of Heap-Manipulating Programs. - Cristian Gherghina; Cristina David; Shengchao Qin; Wei-Ngan Chin (FM, 2011)

A HIP and SLEEK verification system. - Wei-Ngan Chin; Cristina David; Cristian Gherghina (OOPSLA Companion, 2011)

Immutable specifications for more concise and precise verification. - Cristina David; Wei-Ngan Chin (OOPSLA, 2011)

From Verification to Specification Inference. - Wei-Ngan Chin; Cristina David (TASE, 2012)

Automated verification of shape, size and bag properties via user-defined predicates in separation logic. - Wei-Ngan Chin; Cristina David; Huu Hai Nguyen; Shengchao Qin (Sci. Comput. Program., 2012)

Bi-Abduction with Pure Properties for Specification Inference. - Minh-Thai Trinh; Quang Loc Le; Cristina David; Wei-Ngan Chin (APLAS, 2013)

Model and Proof Generation for Heap-Manipulating Programs. - Martin Brain; Cristina David; Daniel Kroening; Peter Schrammel (ESOP, 2014)

HIPimm: verifying granular immutability guarantees. - Andreea Costea; Asankhaya Sharma; Cristina David (PEPM, 2014)

Expressive program verification via structured specifications. - Cristian Gherghina; Cristina David; Shengchao Qin; Wei-Ngan Chin (Int. J. Softw. Tools Technol. Transf., 2014)

Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs. - Cristina David; Daniel Kroening; Matt Lewis (ESOP, 2015)

Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs. - Cristina David; Daniel Kroening; Matt Lewis (ESOP, 2015)

Synthesising Interprocedural Bit-Precise Termination Proofs (T). - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (ASE, 2015)

Using Program Synthesis for Program Analysis. - Cristina David; Daniel Kroening; Matt Lewis (LPAR, 2015)

Synthesising Interprocedural Bit-Precise Termination Proofs (extended version). - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (CoRR, 2015)

Danger Invariants. - Cristina David; Daniel Kroening; Matt Lewis (CoRR, 2015)

Automatically inferring loop invariants via algorithmic learning. - Yungbum Jung; Soonho Kong; Cristina David; Bow-Yaw Wang; Kwangkeun Yi (Math. Struct. Comput. Sci., 2015)

Danger Invariants. - Cristina David; Pascal Kesseli; Daniel Kroening; Matt Lewis (FM, 2016)

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. - Alessandro Abate; Iury Bessa; Dario Cattaruzza; Lucas C. Cordeiro; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen (CAV (1), 2017)

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. - Alessandro Abate; Iury Bessa; Dario Cattaruzza; Lucas C. Cordeiro; Cristina David; Pascal Kesseli; Daniel Kroening (HSCC, 2017)

DSSynth: an automated digital controller synthesis tool for physical plants. - Alessandro Abate; Iury Bessa; Dario Cattaruzza; Lennon C. Chaves; Lucas C. Cordeiro; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen (ASE, 2017)

Kayak: Safe Semantic Refactoring to Java Streams. - Cristina David; Pascal Kesseli; Daniel Kroening (CoRR, 2017)

Counterexample Guided Inductive Synthesis Modulo Theories. - Alessandro Abate; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen (CAV (1), 2018)

Bit-Precise Procedure-Modular Termination Analysis. - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (ACM Trans. Program. Lang. Syst., 2018)

Program Synthesis for Program Analysis. - Cristina David; Pascal Kesseli; Daniel Kroening; Matt Lewis (ACM Trans. Program. Lang. Syst., 2018)

Keratoconus Detection Algorithm using Convolutional Neural Networks: Challenges. - Alexandru Lavric; Valentin Popa; Cristina David; Cristian Costel Paval (ECAI, 2019)

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)

Synbit: synthesizing bidirectional programs using unidirectional sketches. - Masaomi Yamaguchi; Kazutaka Matsuda; Cristina David; Meng Wang 002 (Proc. ACM Program. Lang., 2021)

Using graph neural networks for program termination. - Yoav Alon; Cristina David (ESEC/SIGSOFT FSE, 2022)

Decomposition Without Regret (Poster). - Weixin Zhang; Cristina David; Meng Wang (STAF Workshops, 2022)

Decomposition Without Regret. - Weixin Zhang; Cristina David; Meng Wang (CoRR, 2022)

Ownership Guided C to Rust Translation. - Hanliang Zhang; Cristina David; Yijun Yu; Meng Wang 002 (CAV (3), 2023)

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

Conjugate operators for transparent, explorable research outputs. - Joseph Bond; Cristina David; Minh Nguyen; Dominic Orchard; Roly Perera (CoRR, 2024)

Towards Translating Real-World Code with LLMs: A Study of Translating to Rust. - Hasan Ferit Eniser; Hanliang Zhang; Cristina David; Meng Wang 002; Maria Christakis; Brandon Paulsen; Joey Dodds; Daniel Kroening (CoRR, 2024)

Enhancing SQL Query Generation with Neurosymbolic Reasoning. - Henrijs Princis; Cristina David; Alan Mycroft (AAAI, 2025)

Cognacy Queries over Dependence Graphs for Transparent Visualisations. - Joseph Bond; Cristina David; Minh Nguyen; Dominic Orchard; Roly Perera (ESOP (1), 2025)

Quantifying the benefits of code hints for refactoring deprecated Java APIs. - Cristina David; Pascal Kesseli; Daniel Kroening; Hanliang Zhang (SIGSOFT FSE Companion, 2025)

Scalable, Validated Code Translation of Entire Projects using Large Language Models. - Hanliang Zhang; Cristina David; Meng Wang 002; Brandon Paulsen; Daniel Kroening (Proc. ACM Program. Lang., 2025)

Integrating Large Language Models and Reinforcement Learning for Non-linear Reasoning. - Yoav Alon; Cristina David (Proc. ACM Softw. Eng., 2025)

Introduction to the TASE 2023 Special Issue. - Neeraj Kumar Singh; Cristina David; Meng Sun; Meng Wang (Sci. Comput. Program., 2025)

Assessing Correctness in LLM-Based Code Generation via Uncertainty Estimation. - Arindam Sharma; Cristina David (CoRR, 2025)