Publications

Recent

Concurrent Data Structures Made Easy

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

39th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2024). Pasadena, CA, USA, October 2024.

DSLs in Racket: You Want It How, Now?

Yunjeong Lee and Kiran Gopinathan and Ziyi Yang and Matthew Flatt and Ilya Sergey

17th ACM SIGPLAN International Conference on Software Language Engineering (SLE ’24). Pasadena, CA, USA, October 2024.

Compositional Verification of Composite Byzantine Protocols

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

31st ACM Conference on Computer and Communications Security (CCS 2024). Salt Lake City, UT, USA, October 2024.

PDF Code Artefact

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers

David Young and Ziyi Yang and Ilya Sergey and Alex Potanin

38th European Conference on Object-Oriented Programming (ECOOP 2024). Vienna, Austria, September 2024.

Scaling the Evolution of Verified Software

Kiran Gopinathan

PhD Thesis. NUS School of Computing, August 2024.

Mechanised Hypersafety Proofs about Structured Data

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

2024 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024). Copenhagen, Denmark, June 2024.

Simple and Efficient Concurrent Data Structures via Batch Parallelism

Callista Le

Capstone Thesis. Yale-NUS College, 2024.

Program Synthesis with Accumulators

Nay Chi Naing

Capstone Thesis. Yale-NUS College, 2024.

Small Scale Reflection for the Working Lean User

Vladimir Gladshtein and George Pîrlea and Ilya Sergey

Unpublished draft. 2024.

Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic

Qiyuan Zhao and Zhendong Ang and Umang Mathur and Ilya Sergey

13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). London, UK, January 2024. Distinguished Paper Award.

PDF Code Artefact

Greybox Fuzzing of Distributed Systems

Ruijie Meng and George Pîrlea and Abhik Roychoudhury and Ilya Sergey

30th ACM Conference on Computer and Communications Security (CCS 2023). Copenhagen, Denmark, December 2023.

PDF Code

Adventure of a Lifetime: Extract Method Refactoring for Rust

Sewen Thy and Andreea Costea and Kiran Gopinathan and Ilya Sergey

38th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2023). Lisbon, Portugal, October 2023.

Mostly Automated Proof Repair for Verified Libraries

Kiran Gopinathan and Mayank Keoliya and Ilya Sergey

2023 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023). Orlando, FL, USA, June 2023. ACM SIGPLAN Distinguished Paper Award

Leveraging Rust Types for Program Synthesis

Jonas Fiala and Shachar Itzhaky and Peter Müller and Nadia Polikarpova and Ilya Sergey

2023 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023). Orlando, FL, USA, June 2023. Distinguished Artifact Award

Borrowing without Sorrowing: Implementing Extract Method Refactoring for Rust

Sewen Thy

Capstone Thesis. Yale-NUS College, 2023. Recipient of the Outstanding Yale-NUS Capstone Prize for 2023.

Formally Verifying Accountable Byzantine Consensus

Karolina Grzeszkiewicz

Capstone Thesis. Yale-NUS College, 2023.

Concurrent Structures and Effect Handlers: A Batch Made in Heaven

Koon Wen Lee

Capstone Thesis. Yale-NUS College, 2023.

HIPPODROME: Data Race Repair using Static Analysis Summaries

Andreea Costea and Abhishek Tiwari and Sigmund Chianasta and Kishore R and Abhik Roychoudhury and Ilya Sergey

ACM Transactions on Software Engineering and Methodology. 2023.

Random Testing of a Higher-Order Blockchain Language (Experience Report)

Tram Hoang and Anton Trunov and Leonidas Lampropoulos and Ilya Sergey

27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022). Ljubljana, Slovenia, September 2022.

From C towards Idiomatic & Safer Rust through Constraints-Guided Refactoring

Bryan Tan Yao Hong

MComp Thesis. NUS School of Computing, 2022.

Synthesizing Musical Harmony using Equality Graphs

Juwon Lee

Capstone Thesis. Yale-NUS College, 2022.

Verifying Distributed Protocols: From Executable to Decidable

Mark Yuen

Capstone Thesis. Yale-NUS College, 2022.

A Lazy Desugaring System for Evaluating Programs with Sugars

Ziyi Yang and Yushuo Xiao and Zhichao Guan and Zhenjiang Hu

16th International Symposium on Functional and Logic Programming (FLOPS 2022). Taking place virtually, May 2022.

The Next 700 Smart Contract Languages

Ilya Sergey

Principles of Blockchain Systems 2021. Pages 69–94. Morgan & Claypool. Author’s version.

Certifying the Synthesis of Heap-Manipulating Programs

Yasunari Watanabe and Kiran Gopinathan and George Pîrlea and Nadia Polikarpova and Ilya Sergey

26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021). Taking place virtually, August 2021.

PDF Artefact Video

GopCaml: A Structural Editor for OCaml

Kiran Gopinathan

2021 OCaml Users and Developers Workshop (OCaml 2021). Taking place virtually, August 2021.

Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities (Invited Paper)

Shachar Itzhaky and Hila Peleg and Nadia Polikarpova and Reuben Rowe and Ilya Sergey

33rd International Conference on Computer-Aided Verification (CAV 2021). Taking place virtually, July 2021.

Practical Smart Contract Sharding with Ownership and Commutativity Analysis

George Pîrlea and Amrit Kumar and Ilya Sergey

2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021). Taking place virtually, June 2021.

Cyclic Program Synthesis

Shachar Itzhaky and Hila Peleg and Nadia Polikarpova and Reuben Rowe and Ilya Sergey

2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021). Taking place virtually, June 2021. ACM SIGPLAN Distinguished Paper Award.

A Framework for Certified Program Synthesis

Yasunari Watanabe

MComp Thesis. NUS School of Computing, 2021.

Testing Static Code Analyses with Monadic Definitional Interpreters

Tram Hoang

Capstone Thesis. Yale-NUS College, 2021.

Towards Enhancing Deductive Synthesis of Heap-Manipulating Programs with Examples

Bryan Tan Yao Hong

Capstone Thesis. Yale-NUS College, 2021.

Towards User-Friendly Linearizability Checking

Alaukik Nath Pant

Capstone Thesis. Yale-NUS College, 2021.

A Study of Control and Type-Flow Analyses for Higher-Order Programming Languages

Gabriel Petrov

Capstone Thesis. Yale-NUS College, 2021.

Towards Locally-Parallel Processing of Smart Contract Transactions

Nicholas Chin Jian Wei

Capstone Thesis. Yale-NUS College, 2021.

Automated Repair of Heap-Manipulating Programs using Deductive Synthesis

Thanh-Toan Nguyen and Quang-Trung Ta and Ilya Sergey and Wei-Ngan Chin

22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021). Copenhagen, Denmark, January 2021.

Protocol Combinators for Modeling, Testing, and Execution of Distributed Systems

Kristoffer Just Arndal Andersen and Ilya Sergey

Accepted for publication in Journal of Functional Programming in 2021. Cambridge University Press.

Building a Certified Program Synthesizer

Yasunari Watanabe

Capstone Thesis. Yale-NUS College, 2020. Recipient of the Outstanding Yale-NUS Capstone Prize for 2020.

Compiling a Higher-Order Smart Contract Language to LLVM

Vaivaswatha Nagaraj and Jacob Johannsen and Anton Trunov and George Pîrlea and Amrit Kumar and Ilya Sergey

2020 Virtual LLVM Developers’ Meeting on the LLVM Compiler Infrastructure, October 2020.

Certifying Certainty and Uncertainty in Approximate Membership Query Structures

Kiran Gopinathan and Ilya Sergey

32nd International Conference on Computer-Aided Verification (CAV 2020). Los Angeles, CA, USA, July 2020.

PDF GitHub

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers

Andreea Costea and Amy Zhu and Nadia Polikarpova and Ilya Sergey

29th European Symposium on Programming (ESOP 2020). Dublin, Ireland, April 2020.

PDF GitHub

Safer Smart Contract Programming with Scilla

Ilya Sergey and Vaivaswatha Nagaraj and Jacob Johannsen and Amrit Kumar and Anton Trunov and Ken Chan Guan Hao

34th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2019). Athens, Greece, October 2019. Distinguished Artifact Award.

PDF GitHub Slides Video

Toychain: Formally Verified Blockchain Consensus

George Pîrlea

MEng Thesis. University College London, 2019

PDF Code

Synchronisation Primitives for Smart Contracts

Jake Si Yuan Goh

Capstone Thesis. Yale-NUS College, 2019.

Modelling and Testing Composite Byzantine-Fault Tolerant Consensus Protocols

Daniel Lok

Capstone Thesis. Yale-NUS College, 2019.

QED at Large: A Survey of Engineering of Formally Verified Software

Talia Ringer and Karl Palmskog and Ilya Sergey and Milos Gligoric and Zachary Tatlock

Found. Trends Program. Lang. 2019. Vol. 5, (2-3), Pages 102–281.

PDF Errata

Exploiting the laws of order in smart contracts

Aashish Kolluri and Ivica Nikolic and Ilya Sergey and Aquinas Hobor and Prateek Saxena

ISSTA 2019

Distributed Protocol Combinators

Kristoffer Just Arndal Andersen and Ilya Sergey

PADL 2019

PDF Code

Towards Mechanising Probabilistic Properties of a Blockchain

Kiran Gopinathan and Ilya Sergey

CoqPL 2019

PDF Code Slides

Structuring the Synthesis of Heap-Manipulating Programs

Nadia Polikarpova and Ilya Sergey

46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Lisbon, Portugal, January 2019. ACM SIGPLAN Distinguished Paper Award

PDF GitHub Slides

A True Positives Theorem for a Static Race Detector

Nikos Gorogiannis and Peter O'Hearn and Ilya Sergey

46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Lisbon, Portugal, January 2019.

Finding The Greedy, Prodigal, and Suicidal Contracts at Scale

Ivica Nikolic and Aashish Kolluri and Ilya Sergey and Prateek Saxena and Aquinas Hobor

ACSAC 2018

PDF Code

RacerD: Compositional Static Race Detection

Sam Blackshear and Nikos Gorogiannis and Peter O'Hearn and Ilya Sergey

33rd ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2018). Boston, MA, USA, November 2018.

PDF Video

Temporal Properties of Smart Contracts

Ilya Sergey and Amrit Kumar and Aquinas Hobor

ISoLA. 2018

Paxos Consensus, Deconstructed and Abstracted

‪Álvaro García-Pérez and Alexey Gotsman and Yuri Meshman and Ilya Sergey

ESOP. 2018

Mechanising Blockchain Consensus

George Pîrlea and Ilya Sergey

7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). Los Angeles, CA, USA, January 2018.

PDF GitHub Slides

Programming and Proving with Distributed Protocols

Ilya Sergey and James R. Wilcox and Zachary Tatlock

45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018). Los Angeles, CA, USA, January 2018.

PDF GitHub Slides

A Concurrent Perspective on Smart Contracts

Ilya Sergey and Aquinas Hobor

1st Workshop on Trusted Smart Contracts. 2017

PDF Slides

Programming Language Abstractions for Modularly Verified Distributed Systems

James R. Wilcox and Ilya Sergey and and Zachary Tatlock

SNAPL 2017

PDF Slides
VERSE
Verified Systems Engineering
Yale-NUS College
NUS School of Computing