Ilya Sergey

I am a tenured Associate Professor at the School of Computing of National University of Singapore, where I lead the VERSE lab as a part of PLSE@NUS group. I am also a Research Consultant at Mysten Labs.

I do research in programming languages, software verification, distributed systems, and program synthesis. I am the recipient of the AITO Dahl-Nygaard Junior Prize 2019. I serve as the General Chair for ICFP’25. I designed and co-developed Scilla programming language and organised the ICFP Programming Contest 2019. In the past, I contributed to Facebook Infer and Glasgow Haskell Compiler. Very long time ago, I used to work on Scala and Clojure language support in IntelliJ IDEA.

In 2018-2024, I held a joint appointment at Yale-NUS College. Before moving to Singapore, I was a faculty at University College London. Prior to that, I was a postdoc at IMDEA Software Institute. I hold a PhD in Computer Science from KU Leuven, and an MSc in mathematics from St Petersburg University. Before joining academia I worked as a software engineer at JetBrains.

Short bio in plain text and 3rd person

coordinates

Postal Address:	School of Computing, National University of Singapore COM1, 13 Computing Drive, Singapore 117417
Email:
Office:	COM3-02-56
Office Phone:	+65 6601 1466
Availability:	Outlook Calendar

announcements

Multiple postdoc positions are available in the 5-year MOE Tier 3 project on automated program repair via static analysis and verification. Check out the project page for the details and get in touch!
I am actively looking for motivated PhD students who would like to work on software analysis, verification, and certified synthesis, applying those techniques to concurrent and distributed systems. Feel free to email me if you'd like to chat about research opportunities (please, check the lab page for the relevant topics first) and apply here. The application deadlines are 15 June and 15 December.
Research internships: In case if you are interested in an internship, please send me an email with your CV and a paragraph of text describing your specific interests in the topics of my reseatch (see the VERSE lab page for more details). Strong background in PL/logic/verification or systems-building is a must. Prospective internship candidates will have to complete a pre-interview verification assignment.

news

Apr 14, 2025	We are excited to release Veil, a new framework for verifying distributed protocols, automatically and interactively, in Lean! The accompanying paper (with George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, and Qiyuan Zhao) will appear at the CAV’25.
Feb 21, 2025	Our paper on synthesising Separation Logic predicates using Answer Set Programming (with Ziyi Yang) is accepted at OOPSLA’25.
Jan 24, 2025	Our work on programming language synthesis for automated exploit generation (with Yuxi Ling, Gokul Rajiv, and Kiran Gopinathan) will appear at the 34th USENIX Security Symposium.
Jan 10, 2025	All materials for my Yale-NUS course on Parallel, Concurrent, and Distributed Programming are now publicly available.
Oct 29, 2024	Together with Yong Kiam Tan, we are organising the first Singapore Programming Language Summit, which will take place on 4 December 2024. Please, register by November 8 if you’d like to attend and give a talk.
Oct 2, 2024	I am excited to serve as the General Chair for ICFP’25 and as the Local Chair for the joint ICFP/SPLASH’25 conference, which will take place in Singapore on 12-18 October 2025.
Aug 27, 2024	Our paper on implementing concurrent data structures via batch-parallelism (joint work with Callista Le, Kiran Gopinathan, Koon Wen Lee, and Seth Gilbert) will appear at OOPSLA’24.
Aug 24, 2024	Our work on compositionally verying safety and liveness of BFT protocols (with Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, and Seth Gilbert) will be presented at CCS’24.

selected publications

Veil: A Framework for Automated and Interactive Verification of Transition Systems

George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey

CAV 2025. Springer.

PDF Code Artifact
Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis

Yuxi Ling, Gokul Rajiv, Kiran Gopinathan, and Ilya Sergey

USENIX Security Symposium 2025. USENIX Association.

PDF Artifact
Concurrent Data Structures Made Easy

Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, and Ilya Sergey

Proc. ACM Program. Lang. 2024. (OOPSLA), ACM.

PDF arXiv Code Artifact Slides
Compositional Verification of Composite Byzantine Protocols

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

31st ACM Conference on Computer and Communications Security (CCS’24) 2024. ACM.

PDF Code Artifact
Mechanised Hypersafety Proofs about Structured Data

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

Proc. ACM Program. Lang. 2024. (PLDI), ACM.

PDF arXiv Code Artifact
Mostly Automated Proof Repair for Verified Libraries

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

Proc. ACM Program. Lang. 2023. (PLDI), ACM.

ACM SIGPLAN Distinguished Paper Award

PDF Code Artifact Slides Video Website

lecture notes

Programs and Proofs: Mechanizing Mathematics with Dependent Types

Ilya Sergey

Lecture notes with exercises.

PDF Webpage GitHub

miscellanea

Last time I checked, my Erdős number was 4.

Here is a high-resolution "official" photo of me, suitable for appropriate occasions. Just in case, here's a more casual picture, couresy of Elena Alhimovich. Yet another old picture of mine by Jorge Cham, for I have contributed to the PHD Movie 2 on Kickstarter.

While living in Madrid, I enjoyed its inimitable atmosphere and delicious food. For the latter, this Maribel's Dining Guide to Madrid (kindly provided by Aleks Nanevski) always came in handy.