Andreea Costea

Research Fellow

Programming Languages Lab
School of Computing
National University of Singapopre

andreeac AT comp nus edu sg

Research Interests

My primary research interests revolve around the programming language design and implementation. I am particularly interested in the area of software verification for critical code. More specifically, I've been involved in a series of verification projects which target the memory safety of heap-manipulating programs.


Jul 2020. Thanks Zhengqun Koo , Fadi Faris and Ng Jie Wu for your contributions to HIP/SLEEK and TeachHIP during the 2020 summer intership. Despite the inconvenience of WFH, you guys did a great job!
Jan 2020. Our work on enhancing program synthesis with read-only permissions has been accepted for publication at ESOP 2020. Check out the technical report and accompanying tool - ROBoSuSLik.
Oct 2019. Our project on trustworthy distributed software was awarded a 2.5 years worth of funding from NSoE-TSS !

Publications and Posters

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers [PDF, GitHub ]
Andreea Costea, Amy Zhu, Nadia Polikarpova, and Ilya Sergey. ESOP 2020: 141-168

Automated Modular Verification for Relaxed Communication Protocols [PDF, TOOL ]
Andreea Costea, Wei-Ngan Chin, Shengchao Qin, Florin Craciun. APLAS 2018: 284-305

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

Automated Modular Verifictaion for Relaxed Communication Protocols, APLAS 2018, Victoria University, New Zealand December 2018 [SLIDES]

A Session Logic for Relaxed Communication Protocols, Thesis Defense, National University of Singapore, December 2017 [SLIDES]

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


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


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 - 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.


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.


A platform where students can see HIP/SLEEK in action, or in other words a platform to formally specify and verify C programs.

Teaching Experience

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

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, VMCAI'18, CAV'18, CAV'19, POPL'20