Cristina David

I am a Ph.D. student working with Professor Wei-Ngan Chin. My expected graduation date is December 2011.

I obtained my B.S. degree in Computer Science from Politehnica University of Bucharest, Romania.

Immutable Specifications for More Concise and Precise Verification, Cristina David, Wei-Ngan Chin, Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2011.

A HIP and SLEEK Verification System, Wei-Ngan Chin, Cristina David, Cristian Gherghina, OOPSLA Companion, 2011.

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, To Appear in Science of Computer Programming (SCP), Elsevier, 2011.

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

Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, Kwangkeun Yi, In Programming Languages and Systems - Asian Symposium (APLAS), 2010.

A Specification Logic for Exceptions and Beyond Cristian Gherghina, Cristina David, In Automated Technology for Verification and Analysis - International Symposium (ATVA), 2010.

Translation and Optimization for a Core Calculus with Exceptions, Cristina David, Cristian Gherghina, Wei-Ngan Chin, PEPM'09, Savannah, USA, January 2009. [pdf]

Enhancing Modular OO Verification with Separation Logic, Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin, 35th Annual Symposium on Principles of Programming Languages (POPL'08), San Francisco, USA, January 2008. [pdf]

Multiple Pre/Post Specifications for Heap-Manipulating Methods, Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin, 10th IEEE High Assurance Systems Engineering Symposium (HASE'07), Dallas, Texas, November 2007. [pdf]

Automated Verification of Shape, Size and Bag Properties, Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin, 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'07), Auckland, New Zealand, July 2007. [pdf]

Automated Verification of Shape and Size Properties via Separation Logic, Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin, Eighth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), Nice, France, January 2007. [pdf]

Verification of memory safety and structural and quantitative properties of data structures [HIP]: Collaborated to the design and implementation of a verification system based on separation logic for proving shape, size and bag properties of data structures, as well as detecting invalid memory accesses. The prototype system is built using OCaml and it was used to check programs handling complex data structures, such as sorted linked lists, AVL trees, red-black trees. The proof obligations are discharged with the use of Omega Calculator, CVC, Isabelle, and MONA.

Entailment prover for separation logic [SLEEK]: Contributed to the design and implementation of a prover for separation logic with frame inferring capability. The prototype system is built using OCaml.

Verification of object-oriented programs: Contributed to the design of a new approach for the verification of object-oriented programs that focuses on providing both a static and a dynamic specification, together with a new subsumption relation between specifications in separation logic. This approach gives better precision with less unnecessary re-verifications.

Core calculus for exception handling: Helped in designing a core calculus with unified control flows. Formalized both a small-step and a big-step operational semantics for the calculus, designed its type system and proved type safety. I also help the design some high-level optimization rules and proved their soundness.

National University of Singapore

Teaching Assistant: Fall 2011
Graduate course, CS6202 "Advanced Topics in Programming Languages" (lecturer Wei-Ngan Chin).

Guest Lecturer: Spring 2011
One lecture on the topic "Enhanced Specification Expressivity for Verification with Separation Logic" , graduate course, CS5218 "Principles of Program Analysis" (lecturer Siau-Cheng Khoo)

Teaching Assistant: Fall 2007
Graduate course, CS2104 "Programming Language Concepts" (lecturer Wei-Ngan Chin).

Teaching Assistant: Spring 2007
Graduate course, CS2104 "Programming Language Concepts" (lecturer Wei-Ngan Chin).