Andreea

Andreea Costea

PhD student

Programming Languages Lab
School of Computing
National University of Singapopre

a...@comp.nus.edu.sg

Research Interests

I am particularly interested in the area of software verification of critical code. More specifically, I've been involved in a series of verification projects which target the memory safety of heap-manipulating programs.


My thesis advisor is Prof. Wei-Ngan Chin.

Publications and Posters

A Logic for Multiparty Protocols with Explicit Synchronization [under submission]
Andreea Costea, Florin Craciu, Shengchao Qin, Wei-Ngan Chin.


Towards A Logic for Multiparty Protocols [POSTER]
Andreea Costea, Wei-Ngan Chin. APLAS 2016


Certified Reasoning with Infinity [PDF]
Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, Wei-Ngan Chin. FM 2015: 496-513


Towards a Session Logic for Communication Protocols [PDF]
Florin Craciun, Tibor Kiss, Andreea Costea. ICECCS 2015: 140-149


HIPimm - verifying granular immutability guarantees [PDF]
Andreea Costea, Asankhaya Sharma, Cristina David: PEPM 2014: 189-194

Selected Talks

A Session Logic for Multiparty Protocols with Explicit Synchronization, National Institute of Informatics, Tokyo, Japan, March 2017 [SLIDES]


Towards a Session Logic for Multiparty Protocols, 2nd Workshop on New and Emerging Results in Programming Languages and Systems, HaLong Bay, Vietnam, Nov 2016 [SLIDES]


A Session Logic for Communication Protocols, Oracle Labs, Safety and Security Analysis team, Brisbane, Australia, Dec 2015 [SLIDES]


Towards a Session Logic for Communication Protocols, 17th International Conference on Formal Engineering Methods, Brisbane, Australia, Nov 2015 [SLIDES]


HIPimm: Verifying Granular Immutability Guarantees, Partial Evaluation and Program Manipulation, San Diego, California, Jan 2014 [SLIDES]


Selected Projects

ProtoHIP

The implementation of a logic for multiparty session protocols, which offers support for communication specification and verification.


Omega++

Omega++ is a Coq-certified decision procedure for Presburger arithmetic extended with +infinity and -infinity. With the use of Omega++, we are now able to reason about coinductive data types and infinite data structures (assuming lazy evaluation).


HIPimm

HIPimm - an extension of HIP/SLEEK - offers immutability guarantees at data field level to ensure safe resource sharing for heap-manipulating programs. We can verify program properties such as preservation of data structures shapes in the context of value mutation, flexible aliases, and information leakage prevention.


HIP/SLEEK

Automatic verification framework for heap manipulating programs. HIP is a Hoare-style forward verifier for imperative language, able to modularly check functional correctness and safety properties. SLEEK is an automatic prover for separation logic with frame inferring capability.

Teaching Experience

CS3234 - Logic and Formal Systems - Guest Lecture and Tutorial, Spring 2017

CS3234 - Logic and Formal Systems - Guest Lecture and Tutorial, Spring 2016

CS3234 - Logic and Formal Systems - Guest Tutorial, Spring 2015

CS4215 - Programming Language Implementation - Teaching Assistant, Spring 2015

Science Mentorship Programme NUS-SMP - Co-Mentor, 2011

Other Activities

External Reviewer for: FM’10, VMCAI’12, CPP’12, SAS’13, ICFEM’13, FM’14, APLAS’14, OOPSLA'16, VMCAI'17, CAV'17