| 2026 | CAV | Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean. | Vladimir Gladshtein, Vitaly Kurin, Yueyang Feng, Dipesh Kafle, George Prlea, Qiyuan Zhao, Ilya Sergey |
| 2026 | ITP | Lazy Proof Automation for Separation Logic. | Valentin Mikhalchuk, Vladimir Gladshtein, Ilya Sergey |
| 2025 | CAV | Accelerating Automated Program Verifiers by Automatic Proof Localization. | Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Mller, Markus Pschel, Ilya Sergey |
| 2025 | CAV | Veil: A Framework for Automated and Interactive Verification of Transition Systems. | George Prlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, Ilya Sergey |
| 2024 | CCS | Compositional Verification of Composite Byzantine Protocols. | Qiyuan Zhao, George Prlea, Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey |
| 2024 | CPP | Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. | Qiyuan Zhao, George Prlea, Zhendong Ang, Umang Mathur, Ilya Sergey |
| 2024 | ECOOP | Higher-Order Specifications for Deductive Synthesis of Programs with Pointers. | David Young, Ziyi Yang, Ilya Sergey, Alex Potanin |
| 2024 | SLE | DSLs in Racket: You Want It How, Now? | Yunjeong Lee, Kiran Gopinathan, Ziyi Yang, Matthew Flatt, Ilya Sergey |
| 2023 | CCS | Greybox Fuzzing of Distributed Systems. | Ruijie Meng, George Prlea, Abhik Roychoudhury, Ilya Sergey |
| 2021 | CAV | Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). | Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey |
| 2021 | PLDI | Cyclic program synthesis. | Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey |
| 2021 | PLDI | Practical smart contract sharding with ownership and commutativity analysis. | George Prlea, Amrit Kumar, Ilya Sergey |
| 2021 | VMCAI | Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis. | Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin |
| 2020 | CAV | Certifying Certainty and Uncertainty in Approximate Membership Query Structures. | Kiran Gopinathan, Ilya Sergey |
| 2020 | ESOP | Concise Read-Only Specifications for Better Synthesis of Programs with Pointers. | Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey |
| 2019 | ISSTA | Exploiting the laws of order in smart contracts. | Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena |
| 2019 | PADL | Distributed Protocol Combinators. | Kristoffer Just Arndal Andersen, Ilya Sergey |
| 2019 | PODC | Engineering Distributed Systems that We Can Trust (and Also Run). | Ilya Sergey |
| 2019 | VECoS | Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. | Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey |
| 2018 | ACSAC | Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. | Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor |
| 2018 | ATVA | EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. | Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey |
| 2018 | CPP | Mechanising blockchain consensus. | George Prlea, Ilya Sergey |
| 2018 | ESOP | Paxos Consensus, Deconstructed and Abstracted. | lvaro Garca-Prez, Alexey Gotsman, Yuri Meshman, Ilya Sergey |
| 2018 | ISoLA | Temporal Properties of Smart Contracts. | Ilya Sergey, Amrit Kumar, Aquinas Hobor |
| 2017 | ECOOP | Concurrent Data Structures Linked in Time. | Germn Andrs Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2017 | FC | A Concurrent Perspective on Smart Contracts. | Ilya Sergey, Aquinas Hobor |
| 2016 | ICFP | Experience report: growing and shrinking polygons for random testing of computational geometry algorithms. | Ilya Sergey |
| 2016 | OOPSLA | Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germn Andrs Delbianco |
| 2015 | ESOP | Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2015 | PLDI | Mechanized verification of fine-grained concurrent programs. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2014 | ESOP | Communicating State Transition Systems for Fine-Grained Concurrent Resources. | Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germn Andrs Delbianco |
| 2014 | PEPM | Deriving interpretations of the gradually-typed lambda calculus. | lvaro Garca-Prez, Pablo Nogueira, Ilya Sergey |
| 2014 | POPL | Modular, higher-order cardinality analysis in theory and practice. | Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones |
| 2013 | PEPM | Fixing idioms: a recursion primitive for applicative DSLs. | Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens |
| 2013 | PLDI | Monadic abstract interpreters. | Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens |
| 2012 | ESOP | Gradual Ownership Types. | Ilya Sergey, Dave Clarke |
| 2012 | ICFP | Introspective pushdown analysis of higher-order programs. | Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn |
| 2012 | MPC | Calculating Graph Algorithms for Dominance and Shortest Path. | Ilya Sergey, Jan Midtgaard, Dave Clarke |
| 2009 | ECOOP | A semantics for context-oriented programming with layers. | Dave Clarke, Ilya Sergey |