Publications

Recent

Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
Thanh-Toan Nguyen, Quang-Trung Ta, 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 Outstanding Yale-NUS Capstone Prize for 2020.

Compiling a Higher-Order Smart Contract Language to LLVM
Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea, 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.

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
Andreea Costea, Amy Zhu, Nadia Polikarpova and Ilya Sergey

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

Safer Smart Contract Programming with Scilla
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, 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.

Toychain: Formally Verified Blockchain Consensus
George Pîrlea

MEng Thesis. University College London, 2019

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, Karl Palmskog, Ilya Sergey, Milos Gligoric and Zachary Tatlock

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

Exploiting the laws of order in smart contracts
Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor and Prateek Saxena

ISSTA 2019

Distributed Protocol Combinators
Kristoffer Just Arndal Andersen and Ilya Sergey

PADL 2019

Towards Mechanising Probabilistic Properties of a Blockchain
Kiran Gopinathan and Ilya Sergey

CoqPL 2019

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.

A True Positives Theorem for a Static Race Detector
Nikos Gorogiannis, 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, Aashish Kolluri, Ilya Sergey, Prateek Saxena and Aquinas Hobor

ACSAC 2018

RacerD: Compositional Static Race Detection
Sam Blackshear, Nikos Gorogiannis, 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.

Temporal Properties of Smart Contracts
Ilya Sergey, Amrit Kumar and Aquinas Hobor

ISoLA. 2018

Paxos Consensus, Deconstructed and Abstracted
‪Álvaro García-Pérez, Alexey Gotsman, 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.

Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox and Zachary Tatlock

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

A Concurrent Perspective on Smart Contracts
Ilya Sergey and Aquinas Hobor

1st Workshop on Trusted Smart Contracts. 2017

Programming Language Abstractions for Modularly Verified Distributed Systems
James R. Wilcox, Ilya Sergey and and Zachary Tatlock

SNAPL 2017

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