Ilya Sergey

Associate Professor at National University of Singapore


I am a tenured Associate Professor at the School of Computing of National University of Singapore, where I run the VERSE research group as a part of PLSE@NUS lab. I also hold a joint appointment at Yale-NUS College.

I do research in programming language design and implementation, software verification, distributed systems, program synthesis and repair. I am the recipient of the AITO Dahl-Nygaard Junior Prize 2019. I designed and co-developed Scilla, a programming language for safe smart contracts, used by Zilliqa. I 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.

Before moving to Singapore, I was a faculty at University College London in 2015-2018. 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 6516 1903
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 and apply here. The next application deadline is 15 June 2023.

news

May 26, 2023 Two awards at the upcoming PLDI’23:
  • Our paper about Sisyphus has won an ACM SIGPLAN Distinguished Paper Award (8 out of 83 accepted papers awarded).
  • The implementation of RusSOL has won a Distinguished Artifact Award (single award given out of 67 submitted artifacts).
Apr 7, 2023 Two papers accepted at PLDI’23:
Mar 17, 2023 I’ve had great time visiting CISPA (hosted by Swen Jacobs), where I gave a talk on the current state of the SuSLik synthesiser.
Mar 12, 2023 I have participated in the Dagstuhl Seminar on Unifying Formal Methods for Trustworthy Distributed Systems, which we have co-organised with Roopsha Samanta, Swen Jacobs, and Ken McMillan. It was fun.
Sep 21, 2022 I am thrilled to participate in the Workshop on Dependable and Secure Software Systems that will take place at ETH Zurich on October 7-8. I will present our work on sharding smart contracts.
Jul 20, 2022 I’m delighted to be amongst the recipients of the Fall 2021 Amazon Research Award.
Jul 18, 2022 Vladimir Gladstein joins VERSE lab as a PhD student. Welcome, Vladimir!
Jul 1, 2022 Our paper on random testing of Scilla interpreter and compiler with QuickChick (co-authored with Tram Hoang, Anton Trunov, and Leonidas Lampropoulos) will appear at ICFP’22.

selected publications

  1. Mostly Automated Proof Repair for Verified Libraries
    Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey
    Proc. ACM Program. Lang. 2023. Vol. 7, (PLDI), Pages 107:1–107:25. ACM.
    ACM SIGPLAN Distinguished Paper Award
    PDF Code Artifact Website
  2. Leveraging Rust Types for Program Synthesis
    Jonáš Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, and Ilya Sergey
    Proc. ACM Program. Lang. 2023. Vol. 7, (PLDI), Pages 164:1–164:24. ACM.
    Distinguished Artifact Award
    PDF Extended Version Artifact
  3. Cyclic Program Synthesis
    Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben Rowe, and Ilya Sergey
    PLDI 2021. Pages 944–959. ACM.
    ACM SIGPLAN Distinguished Paper Award
    PDF Extended Version Artifact
  4. Practical Smart Contract Sharding with Ownership and Commutativity Analysis
    George Pîrlea, Amrit Kumar, and Ilya Sergey
    PLDI 2021. Pages 1327–1341. ACM.
    PDF Artifact
  5. Certifying Certainty and Uncertainty in Approximate Membership Query Structures
    Kiran Gopinathan, and Ilya Sergey
    CAV 2020. LNCS, Vol. 12225, Pages 279–303. Springer.
    PDF Code Artifact Blog Slides Video
  6. Safer Smart Contract Programming with Scilla
    Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao
    Proc. ACM Program. Lang. 2019. Vol. 3, (OOPSLA), Pages 185:1–185:30. ACM.
    Distinguished Artifact Award
    PDF Code Artifact Slides Video
  7. Structuring the Synthesis of Heap-Manipulating Programs
    Nadia Polikarpova, and Ilya Sergey
    Proc. ACM Program. Lang. 2019. Vol. 3 (POPL), Pages 72:1–72:30. ACM.
    ACM SIGPLAN Distinguished Paper Award
    PDF arXiv Code Artifact Slides Video
  8. Programming and Proving with Distributed Protocols
    Ilya Sergey, James R. Wilcox, and Zachary Tatlock
    Proc. ACM Program. Lang. 2018. Vol. 2 (POPL), Pages 28:1–28:30. ACM.
    PDF Code Slides

lecture notes

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