Cristina David

66 papers A* 4A 5B 8C 2Misc 3Journal 34Unranked 10
YearRankTypeTitle / Venue / Authors
2026 J jnl
AI-Assisted Authoring for Transparent, Data-Driven Documents.
CoRR
Alfonso Piscitelli, Cristina David, Mattia De Rosa, Ali Mohammed, Federico Nanni, Jacob Pake, Roly Perera, Jessy Sodimu, Chenyiqiu Zheng
2026 J jnl
Validated Code Translation for Projects with External Libraries.
CoRR
Hanliang Zhang, Arindam Sharma, Cristina David, Meng Wang, Brandon Paulsen, Daniel Kroening, Wenjia Ye, Taro Sekiyama
2025 J jnl
Assessing Correctness in LLM-Based Code Generation via Uncertainty Estimation.
CoRR
Arindam Sharma, Cristina David
2025 — conf
Cognacy Queries over Dependence Graphs for Transparent Visualisations.
ESOP (1)
Joseph Bond, Cristina David, Minh Nguyen, Dominic Orchard, Roly Perera
2025 A* conf
Enhancing SQL Query Generation with Neurosymbolic Reasoning.
AAAI
Henrijs Princis, Cristina David, Alan Mycroft
2025 J jnl
Integrating Large Language Models and Reinforcement Learning for Non-linear Reasoning.
Proc. ACM Softw. Eng.
Yoav Alon, Cristina David
2025 J jnl
Introduction to the TASE 2023 Special Issue.
Sci. Comput. Program.
Neeraj Kumar Singh, Cristina David, Meng Sun, Meng Wang
2025 — conf
Quantifying the benefits of code hints for refactoring deprecated Java APIs.
SIGSOFT FSE Companion
Cristina David, Pascal Kesseli, Daniel Kroening, Hanliang Zhang
2025 J jnl
Scalable, Validated Code Translation of Entire Projects using Large Language Models.
Proc. ACM Program. Lang.
Hanliang Zhang, Cristina David, Meng Wang, Brandon Paulsen, Daniel Kroening
2025 J jnl
TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation.
CoRR
Henrijs Princis, Arindam Sharma, Cristina David
2024 J jnl
Conjugate operators for transparent, explorable research outputs.
CoRR
Joseph Bond, Cristina David, Minh Nguyen, Dominic Orchard, Roly Perera
2024 J jnl
Enhancing SQL Query Generation with Neurosymbolic Reasoning.
CoRR
Henrijs Princis, Cristina David, Alan Mycroft
2024 J jnl
Integrating Large Language Models and Reinforcement Learning for Non-Linear Reasoning.
CoRR
Yoav Alon, Cristina David
2024 J jnl
Quantifying the benefits of code hints for refactoring deprecated Java APIs.
CoRR
Cristina David, Pascal Kesseli, Daniel Kroening, Hanliang Zhang
2024 J jnl
Scalable, Validated Code Translation of Entire Projects using Large Language Models.
CoRR
Hanliang Zhang, Cristina David, Meng Wang, Brandon Paulsen, Daniel Kroening
2024 J jnl
Towards Translating Real-World Code with LLMs: A Study of Translating to Rust.
CoRR
Hasan Ferit Eniser, Hanliang Zhang, Cristina David, Meng Wang, Maria Christakis, Brandon Paulsen, Joey Dodds, Daniel Kroening
2023 — conf
Ownership Guided C to Rust Translation.
CAV (3)
Hanliang Zhang, Cristina David, Yijun Yu, Meng Wang
2023 J jnl
Ownership guided C to Rust translation.
CoRR
Hanliang Zhang, Cristina David, Yijun Yu, Meng Wang
2023 J jnl
Synthesising Programs with Non-trivial Constants.
J. Autom. Reason.
Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
2023 Misc ed.
Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Bristol, UK, July 4-6, 2023, Proceedings
TASE
Cristina David, Meng Sun
2022 — conf
Decomposition Without Regret (Poster).
STAF Workshops
Weixin Zhang, Cristina David, Meng Wang
2022 J jnl
Decomposition Without Regret.
CoRR
Weixin Zhang, Cristina David, Meng Wang
2022 J jnl
Synbit: synthesizing bidirectional programs using unidirectional sketches.
Formal Methods Syst. Des.
Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang
2022 J jnl
Using Graph Neural Networks for Program Termination.
CoRR
Yoav Alon, Cristina David
2022 — conf
Using graph neural networks for program termination.
ESEC/SIGSOFT FSE
Yoav Alon, Cristina David
2021 J jnl
Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches.
CoRR
Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang
2021 J jnl
Synbit: synthesizing bidirectional programs using unidirectional sketches.
Proc. ACM Program. Lang.
Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang
2020 J jnl
Automated formal synthesis of provably safe digital controllers for continuous plants.
Acta Informatica
Alessandro Abate, Iury Bessa, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2019 A conf
Keratoconus Detection Algorithm using Convolutional Neural Networks: Challenges.
ECAI
Alexandru Lavric, Valentin Popa, Cristina David, Cristian Costel Paval
2018 J jnl
Bit-Precise Procedure-Modular Termination Analysis.
ACM Trans. Program. Lang. Syst.
Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter
2018 — conf
Counterexample Guided Inductive Synthesis Modulo Theories.
CAV (1)
Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2018 J jnl
Program Synthesis for Program Analysis.
ACM Trans. Program. Lang. Syst.
Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis
2017 — conf
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants.
CAV (1)
Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2017 J jnl
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants.
CoRR
Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2017 A* conf
DSSynth: an automated digital controller synthesis tool for physical plants.
ASE
Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lennon C. Chaves, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen
2017 J jnl
Kayak: Safe Semantic Refactoring to Java Streams.
CoRR
Cristina David, Pascal Kesseli, Daniel Kroening
2017 — conf
Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants.
HSCC
Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening
2016 B conf
Danger Invariants.
FM
Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis
2016 J jnl
Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants.
CoRR
Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening
2015 J jnl
Automatically inferring loop invariants via algorithmic learning.
Math. Struct. Comput. Sci.
Yungbum Jung, Soonho Kong, Cristina David, Bow-Yaw Wang, Kwangkeun Yi
2015 J jnl
Danger Invariants.
CoRR
Cristina David, Daniel Kroening, Matt Lewis
2015 A conf
Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs.
ESOP
Cristina David, Daniel Kroening, Matt Lewis
2015 A* conf
Synthesising Interprocedural Bit-Precise Termination Proofs (T).
ASE
Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter
2015 J jnl
Synthesising Interprocedural Bit-Precise Termination Proofs (extended version).
CoRR
Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter
2015 A conf
Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs.
ESOP
Cristina David, Daniel Kroening, Matt Lewis
2015 B conf
Using Program Synthesis for Program Analysis.
LPAR
Cristina David, Daniel Kroening, Matt Lewis
2015 J jnl
Using Program Synthesis for Program Analysis.
CoRR
Cristina David, Daniel Kroening, Matt Lewis
2014 J jnl
Expressive program verification via structured specifications.
Int. J. Softw. Tools Technol. Transf.
Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin
2014 C conf
HIPimm: verifying granular immutability guarantees.
PEPM
Andreea Costea, Asankhaya Sharma, Cristina David
2014 A conf
Model and Proof Generation for Heap-Manipulating Programs.
ESOP
Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel
2014 J jnl
Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs.
CoRR
Cristina David, Daniel Kroening, Matt Lewis
2014 J jnl
Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs.
CoRR
Cristina David, Daniel Kroening, Matt Lewis
2013 B conf
Bi-Abduction with Pure Properties for Specification Inference.
APLAS
Minh-Thai Trinh, Quang Loc Le, Cristina David, Wei-Ngan Chin
2012 J jnl
Automated verification of shape, size and bag properties via user-defined predicates in separation logic.
Sci. Comput. Program.
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin
2012 Misc conf
From Verification to Specification Inference.
TASE
Wei-Ngan Chin, Cristina David
2011 — conf
A HIP and SLEEK verification system.
OOPSLA Companion
Wei-Ngan Chin, Cristina David, Cristian Gherghina
2011 A conf
Immutable specifications for more concise and precise verification.
OOPSLA
Cristina David, Wei-Ngan Chin
2011 B conf
Structured Specifications for Better Verification of Heap-Manipulating Programs.
FM
Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin
2010 B conf
A Specification Logic for Exceptions and Beyond.
ATVA
Cristian Gherghina, Cristina David
2010 B conf
Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates.
APLAS
Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, Kwangkeun Yi
2009 Misc conf
Automated Verification Using Unified Control Flows.
TASE
Cristian Gherghina, Cristina David
2009 C conf
Translation and optimization for a core calculus with exceptions.
PEPM
Cristina David, Cristian Gherghina, Wei-Ngan Chin
2008 A* conf
Enhancing modular OO verification with separation logic.
POPL
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin
2007 B conf
Automated Verification of Shape and Size Properties Via Separation Logic.
VMCAI
Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin
2007 B conf
Automated Verification of Shape, Size and Bag Properties.
ICECCS
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin
2007 — conf
Multiple Pre/Post Specifications for Heap-Manipulating Methods.
HASE
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin