Ilya Sergey

Publication Activity (10 Years)

Years Active: 2009-2024
Publications (10 Years): 62

Top Topics

State Transition

Distributed Systems

Program Synthesis

Top Venues

Proc. ACM Program. Lang.

Publications

David Young, Ziyi Yang, Ilya Sergey, Alex Potanin
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version). CoRR (2024)
Vladimir Gladshtein, George Pîrlea, Ilya Sergey
Small Scale Reflection for the Working Lean User. CoRR (2024)
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. CPP (2024)
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman P. Amarasinghe, Ilya Sergey
Mechanised Hypersafety Proofs about Structured Data: Extended Version. CoRR (2024)
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman P. Amarasinghe, Ilya Sergey
Mechanised Hypersafety Proofs about Structured Data. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey
Adventure of a Lifetime: Extract Method Refactoring for Rust. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Swen Jacobs, Kenneth McMillan, Roopsha Samanta, Ilya Sergey
Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112). Dagstuhl Reports 13 (3) (2023)
Kiran Gopinathan, Mayank Keoliya, Ilya Sergey
Mostly Automated Proof Repair for Verified Libraries. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Jonás Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey
Leveraging Rust Types for Program Synthesis. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Ruijie Meng, George Pîrlea, Abhik Roychoudhury, Ilya Sergey
Distributed System Fuzzing. CoRR (2023)
Ruijie Meng, George Pîrlea, Abhik Roychoudhury, Ilya Sergey
Greybox Fuzzing of Distributed Systems. CCS (2023)
Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey
Hippodrome: Data Race Repair Using Static Analysis Summaries. ACM Trans. Softw. Eng. Methodol. 32 (2) (2023)
Tram Hoang, Anton Trunov, Leonidas Lampropoulos, Ilya Sergey
Random testing of a higher-order blockchain language (experience report). Proc. ACM Program. Lang. 6 (ICFP) (2022)
Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin
Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis. VMCAI (2021)
Kristoffer Just Arndal Andersen, Ilya Sergey
Protocol combinators for modeling, testing, and execution of distributed systems. J. Funct. Program. 31 (2021)
Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey
HIPPODROME: Data Race Repair using Static Analysis Summaries. CoRR (2021)
George Pîrlea, Amrit Kumar, Ilya Sergey
Practical smart contract sharding with ownership and commutativity analysis. PLDI (2021)
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). CAV (1) (2021)
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey
Cyclic program synthesis. PLDI (2021)
Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey
Certifying the synthesis of heap-manipulating programs. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
QED at Large: A Survey of Engineering of Formally Verified Software. CoRR (2020)
Kiran Gopinathan, Ilya Sergey
Certifying Certainty and Uncertainty in Approximate Membership Query Structures - Extended Version. CoRR (2020)
Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers - Extended Version. CoRR (2020)
Kiran Gopinathan, Ilya Sergey
Certifying Certainty and Uncertainty in Approximate Membership Query Structures. CAV (2) (2020)
Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea, Amrit Kumar, Ilya Sergey
Compiling a Higher-Order Smart Contract Language to LLVM. CoRR (2020)
Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers. ESOP (2020)
Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
A true positives theorem for a static race detector. Proc. ACM Program. Lang. 3 (POPL) (2019)
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. VECoS (2019)
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, Ken Chan Guan Hao
Safer smart contract programming with Scilla. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Nadia Polikarpova, Ilya Sergey
Structuring the synthesis of heap-manipulating programs. Proc. ACM Program. Lang. 3 (POPL) (2019)
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
QED at Large: A Survey of Engineering of Formally Verified Software. Found. Trends Program. Lang. 5 (2-3) (2019)
Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena
Exploiting the laws of order in smart contracts. ISSTA (2019)
Kristoffer Just Arndal Andersen, Ilya Sergey
Distributed Protocol Combinators. PADL (2019)
Ilya Sergey
Engineering Distributed Systems that We Can Trust (and Also Run). PODC (2019)
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
GASTAP: A Gas Analyzer for Smart Contracts. CoRR (2018)
Ilya Sergey, James R. Wilcox, Zachary Tatlock
Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2 (POPL) (2018)
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. ATVA (2018)
George Pîrlea, Ilya Sergey
Mechanising blockchain consensus. CPP (2018)
Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
A True Positives Theorem for a Static Race Detector - Extended Version. CoRR (2018)
Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
RacerD: compositional static race detection. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Ilya Sergey, Amrit Kumar, Aquinas Hobor
Temporal Properties of Smart Contracts. ISoLA (4) (2018)
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. CoRR (2018)
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. CoRR (2018)
Nadia Polikarpova, Ilya Sergey
Structuring the Synthesis of Heap-Manipulating Programs. CoRR (2018)
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. ACSAC (2018)
Ilya Sergey, Amrit Kumar, Aquinas Hobor
Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR (2018)
Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena
Exploiting The Laws of Order in Smart Contracts. CoRR (2018)
Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey
Paxos Consensus, Deconstructed and Abstracted (Extended Version). CoRR (2018)
Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey
Paxos Consensus, Deconstructed and Abstracted. ESOP (2018)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time (Artifact). Dagstuhl Artifacts Ser. 3 (2) (2017)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time. ECOOP (2017)
James R. Wilcox, Ilya Sergey, Zachary Tatlock
Programming Language Abstractions for Modularly Verified Distributed Systems. SNAPL (2017)
Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones, Joachim Breitner
Modular, higher order cardinality analysis in theory and practice. J. Funct. Program. 27 (2017)
Ilya Sergey, Aquinas Hobor
A Concurrent Perspective on Smart Contracts. CoRR (2017)
Ilya Sergey, Aquinas Hobor
A Concurrent Perspective on Smart Contracts. Financial Cryptography Workshops (2017)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. OOPSLA (2016)
Ilya Sergey
Experience report: growing and shrinking polygons for random testing of computational geometry algorithms. ICFP (2016)
Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski
Operational Aspects of C/C++ Concurrency. CoRR (2016)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time. CoRR (2016)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects. CoRR (2015)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP (2015)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Mechanized verification of fine-grained concurrent programs. PLDI (2015)
J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn
Pushdown flow analysis with abstract garbage collection. J. Funct. Program. 24 (2-3) (2014)
Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco
Communicating State Transition Systems for Fine-Grained Concurrent Resources. ESOP (2014)
Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey
Deriving interpretations of the gradually-typed lambda calculus. PEPM (2014)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. CoRR (2014)
Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones
Modular, higher-order cardinality analysis in theory and practice. POPL (2014)
J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn
Pushdown flow analysis with abstract garbage collection. CoRR (2014)
Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens
Fixing idioms: a recursion primitive for applicative DSLs. PEPM (2013)
Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens
Monadic abstract interpreters. PLDI (2013)
Ilya Sergey, Jan Midtgaard, Dave Clarke
Calculating Graph Algorithms for Dominance and Shortest Path. MPC (2012)
Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
Introspective Pushdown Analysis of Higher-Order Programs CoRR (2012)
Ilya Sergey, Dave Clarke
A correspondence between type checking via reduction and type checking via evaluation. Inf. Process. Lett. 112 (1-2) (2012)
Ilya Sergey, Dave Clarke
Gradual Ownership Types. ESOP (2012)
Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
Introspective pushdown analysis of higher-order programs. ICFP (2012)
Ilya Sergey, Dave Clarke
From type checking by recursive descent to type checking with an abstract machine. LDTA (2011)
Dave Clarke, Ilya Sergey
A semantics for context-oriented programming with layers. COP@ECOOP (2009)