Recent
Random Testing of a Higher-Order Blockchain Language (Experience Report)
Tram Hoang, Anton Trunov, Leonidas Lampropoulos and Ilya Sergey
27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022). Ljubljana, Slovenia, September 2022.
HIPPODROME: Data Race Repair using Static Analysis Summaries
Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury and Ilya Sergey
ACM Transactions on Software Engineering and Methodology. 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, Yushuo Xiao, 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, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova and Ilya Sergey
26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021). Taking place virtually, August 2021.
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, Hila Peleg, Nadia Polikarpova, 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, 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, Hila Peleg, Nadia Polikarpova, Reuben Rowe and Ilya Sergey
2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021). Taking place virtually, June 2021. PLDI 2021 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, 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. OOPSLA 2019 Distinguished Artifact Award.
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
Distributed Protocol Combinators
Kristoffer Just Arndal Andersen and Ilya Sergey
Towards Mechanising Probabilistic Properties of a Blockchain
Kiran Gopinathan and Ilya Sergey
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. POPL 2019 Distinguished Paper Award
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
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
Paxos Consensus, Deconstructed and Abstracted
Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman and Ilya Sergey
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
