Ilya SERGEY
Associate Professor- Ph.D. (Computer Science, KU Leuven, Belgium, 2012)
- M.Sc. (Mathematics and Computer Science, Saint Petersburg State University, Russia, 2008)
Ilya Sergey is an Associate Professor at the School of Computing of National University of Singapore, where he leads the Verified Systems Engineering lab. Ilya got his PhD in Computer Science at KU Leuven. Before joining NUS, he was a postdoctoral researcher at IMDEA Software Institute and a faculty at University College London. Prior to becoming an academic, he worked as a software developer at JetBrains. Ilya does research in programming language design and implementation, distributed systems, software verification, and program synthesis. He is a recipient of several distinguished paper awards at POPL and PLDI, the 2019 Dahl-Nygaard Junior Prize, Yale-NUS Distinguished Researcher award, and academic research awards from Google, Facebook, and Amazon.
RESEARCH INTERESTS
Design and Implementation of Programming Languages
Applied Logic for Software Verification
Concurrent and Distributed Systems
RESEARCH PROJECTS
Automated Proof Evolution for Verified Software Systems
This project automates proof evolution for verified software systems, adapting proofs to changing specs and programs. It emphasizes Separation Logic, aiming to advance beyond proof-of-concept stage for real-world systems.
Practical Automated Testing of Distributed Systems
TRL 4
SuSLik
Synthesis of Heap-Manipulating Programs from Separation Logic specifications
RESEARCH GROUPS
Verified Systems Engineering
We do research in the design and implementation of programming languages (PL), mathematical models of computation, and computer-assisted formal reasoning. We investigate the theoretical foundations of programming and build tools for ensuring that certain kinds of costly software errors and vulnerabilities never occur in the real-world code, which many people rely upon in their everyday lives.
TEACHING INNOVATIONS
SELECTED PUBLICATIONS
- Mostly Automated Proof Repair for Verified Libraries. Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey. PLDI'23
- Cyclic Program Synthesis. Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben Rowe, and Ilya Sergey. PLDI'21
- Practical Smart Contract Sharding with Ownership and Commutativity Analysis. George Pîrlea, Amrit Kumar, and Ilya Sergey. PLDI'21
- Certifying Certainty and Uncertainty in Approximate Membership Query Structures. Kiran Gopinathan, and Ilya Sergey. CAV'20
- Safer Smart Contract Programming with Scilla. Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, Ken Chan. OOPSLA'19
- Structuring the Synthesis of Heap-Manipulating Programs. Nadia Polikarpova and Ilya Sergey. POPL'19
- Programming and Proving with Distributed Protocols. Ilya Sergey, James R. Wilcox, and Zachary Tatlock. POPL'18
AWARDS & HONOURS
CPP'24 Distinguished Paper Award for the work "Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic"
Google Research Award (South Asia & Southeast Asia) 2023
ACM SIGPLAN Distinguished Paper Award (PLDI'23) for the work "Mostly Automated Proof Repair for Verified Libraries"
ACM SIGPLAN Distinguished Paper Award (PLDI'21) for the work "Cyclic Program Synthesis"
Yale-NUS Distinguished Researcher Award for 2021
AITO Dahl-Nygaard Junior Prize for 2019
ACM SIGPLAN Distinguished Paper Award (POPL'19) for the work "Structuring the Synthesis of Heap-Manipulating Programs"
Google Faculty Research Award 2017
COURSES TAUGHT
CS4212
Compiler Design