Andreea Costea
Research Fellow
Automated Program Repair @NUS
Software Engineering Lab
Programming Languages Lab
School of Computing
National University of Singapopre
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