Andreea

Andreea Costea

Research Fellow

Automated Program Repair @NUS
Software Engineering Lab
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 languages design and implementation. I am particularly interested in the area of software verification for critical code, program synthesis and automated program repair. More specifically, I've been involved in a series of verification projects which target the memory safety of heap-manipulating programs.


News

Mar 2023. It was exciting participating in the Dagstuhl Seminar on Unifying Formal Methods for Trustworthy Distributed Systems !
Feb 2022. Exciting news: our APR team has been awarded a Ministry of Education Tier 3 grant in order to pursue its vision for the programming experience of tomorrow. Get in touch if we share similar pursuits, if you're a Rustacean wanting to enahnce the Rust ecosystem, or if APR is your cup of tea. Join us!
Jan 2022. Had an inspiring conversation about how to tackle some of the challenges a computer scientist faces at different career stages PLMW @ POPL2022.
Jan 2022. Glad to announce that I have officialy joined the Sofware Engineering group in NUS, working with Abhik Roychoudhury and other enthusiastic researchers on program repair.
Oct 2021. Publicity Chair for SPLASH 2022 .
Jul 2021. Co-chair of the Artifact Evaluation Committee for ESOP 2022 , with KC. Motivated researchers who wish to serve on the AEC, please nominate yourselves by filling up this form.
Jun 2021. Grads and undergrads warmly encouraged to submit a 3-page extended abstract outlining their WIP research to participate in the SRC @ICFP'21.
May 2021. Join us for an “Ask Me Anything!” session with Joxan Jaffar at PLDI'21.
May 2021. Tune in for the Panel Discussion on Grad School at PLMW@PLDI'21 .
April 2021. Congratulations Zhengqun Koo for successfully completing and presenting your FYP!
April 2021. PC for APLAS'21 .
Jan 2021. Panel Discussion on Work/Life Balance at POPL'21 .

Publications and Posters

Adventure of a Lifetime: Extract Method Refactoring for Rust [PDF, GitHub]
Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey. OOPLSA 2023


Protocol Conformance with Choreographic PlusCal [PDF, GitHub]
Darius Foo, Andreea Costea, Chin Wei-Ngan. TASE 2023


Hippodrome: Data Race Repair using Static Analysis Summaries [PDF, GitHub , Artifact , slides]
Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, and Ilya Sergey. ACM Trans. Softw. Eng. Methodol. 2022


Concise Read-Only Specifications for Better Synthesis of Programs with Pointers [PDF, GitHub , slides , video]
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

HIPPODROME

An automated program repair tool for data races in Java Programs. It automatically generates and applies patches validated by Infer to be correct.


ROBoSuSLik

A framework for the synthesis of heap-manipulating programs, where the synthesis is guided by Separation Logic specs enhanced with the logical mechanism of read-only borrows.


Mercurius

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.

TeachHIP

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

Service

Chair: Publicity @ SPLASH 2023, Publicity @ SPLASH 2022, Artefact Evaluation @ ESOP2022, Poster and SRC @ APLAS'19

PC: ICSE'24, ICFP'23, TASE'23, SRC @ ICFP'21, APLAS'21, APLAS'20

Panel discussions: PLMW @ POPL'22, PLDI'21, PLMW @ PLDI'21, POPL'21

External Reviewer for: TOSEM'23, POPL'22, TOSEM'21, POPL'20, TOSEM'19, CAV'19, CAV'18, VMCAI'18, CAV'17, VMCAI'17, OOPSLA'16, APLAS'14, FM'14, ICFEM'13, SAS'13, CPP'12, VMCAI'12, FM'10

Research (co)Mentor:

  • Zhengqun Koo (FYP: AY2020/2021): Towards Bug-Free Distributed Go Programs
  • Sigmund Chianasta (intern: May-Aug 2020): IntelliJ plugin for Infer and Data Race Repair
  • Zhengqun Koo (intern: May - Jul 2020): A decision procedure for reasoning about arrays using Separation Logic
  • Fadi Faris (intern: May - Jul 2020): Web Platform for Teaching Verification with HIP/SLEEK,
  • Ng Jie Wu (intern: May - Jul 2020)
  • Yinfang Chen (Master: AY2019/2020): WaitGroup and CountDownLatch Reasoning
  • Zhengqun Koo (UROP: AY2018/2019): ecce: A Visualizer and Simulator for Session Protocols
  • Xu Jun (FYP: AY 2018/2019): Investigation of Design and Implementation of Domain-Specific Languages
  • Andreea Stoican (Master: 2017): Local Reasoning for Communication-Centered Programs
  • Low Zheng Heng Henry (FYP): Safety for Consensus-Based Systems in Rust
  • Valentina Manea (Master: 2016): Session Logic for Multiparty Sessions