Ilya Sergey

96 papers A* 9A 13B 8C 5Journal 51Unranked 9
YearRankTypeTitle / Venue / Authors
2026 J jnl
Foundational Multi-Modal Program Verifiers.
Proc. ACM Program. Lang.
Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey
2026 J jnl
Grammar Repair with Examples and Tree Automata: Extended Version.
CoRR
Yunjeong Lee, Gokul Rajiv, Ilya Sergey
2025 — conf
Accelerating Automated Program Verifiers by Automatic Proof Localization.
CAV (3)
Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Müller, Markus Püschel, Ilya Sergey
2025 J jnl
Beluga: Block Synchronization for BFT Consensus Protocols.
CoRR
Tasos Kichidis, Lefteris Kokoris-Kogias, Arun Koshy, Ilya Sergey, Alberto Sonnino, Mingwei Tian, Jianting Zhang
2025 B conf
Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference.
ICLP
Ziyi Yang, George Pîrlea, Ilya Sergey
2025 J jnl
Inductive Synthesis of Inductive Heap Predicates - Extended Version.
CoRR
Ziyi Yang, Ilya Sergey
2025 J jnl
Inductive Synthesis of Inductive Heap Predicates.
Proc. ACM Program. Lang.
Ziyi Yang, Ilya Sergey
2025 A* conf
Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis.
USENIX Security Symposium
Yuxi Ling, Gokul Rajiv, Kiran Gopinathan, Ilya Sergey
2025 — conf
Veil: A Framework for Automated and Interactive Verification of Transition Systems.
CAV (3)
George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, Ilya Sergey
2024 A* conf
Compositional Verification of Composite Byzantine Protocols.
CCS
Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey
2024 J jnl
Concurrent Data Structures Made Easy (Extended Version).
CoRR
Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, Ilya Sergey
2024 J jnl
Concurrent Data Structures Made Easy.
Proc. ACM Program. Lang.
Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, Ilya Sergey
2024 B conf
DSLs in Racket: You Want It How, Now?
SLE
Yunjeong Lee, Kiran Gopinathan, Ziyi Yang, Matthew Flatt, Ilya Sergey
2024 J jnl
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact).
Dagstuhl Artifacts Ser.
David Young, Ziyi Yang, Ilya Sergey, Alex Potanin
2024 J jnl
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version).
CoRR
David Young, Ziyi Yang, Ilya Sergey, Alex Potanin
2024 A conf
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers.
ECOOP
David Young, Ziyi Yang, Ilya Sergey, Alex Potanin
2024 J jnl
Mechanised Hypersafety Proofs about Structured Data.
Proc. ACM Program. Lang.
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman P. Amarasinghe, Ilya Sergey
2024 J jnl
Mechanised Hypersafety Proofs about Structured Data: Extended Version.
CoRR
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman P. Amarasinghe, Ilya Sergey
2024 B conf
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic.
CPP
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey
2024 J jnl
Small Scale Reflection for the Working Lean User.
CoRR
Vladimir Gladshtein, George Pîrlea, Ilya Sergey
2023 J jnl
Adventure of a Lifetime: Extract Method Refactoring for Rust.
Proc. ACM Program. Lang.
Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey
2023 J jnl
Distributed System Fuzzing.
CoRR
Ruijie Meng, George Pîrlea, Abhik Roychoudhury, Ilya Sergey
2023 A* conf
Greybox Fuzzing of Distributed Systems.
CCS
Ruijie Meng, George Pîrlea, Abhik Roychoudhury, Ilya Sergey
2023 J jnl
Hippodrome: Data Race Repair Using Static Analysis Summaries.
ACM Trans. Softw. Eng. Methodol.
Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey
2023 J jnl
Leveraging Rust Types for Program Synthesis.
Proc. ACM Program. Lang.
Jonás Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey
2023 J jnl
Mostly Automated Proof Repair for Verified Libraries.
Proc. ACM Program. Lang.
Kiran Gopinathan, Mayank Keoliya, Ilya Sergey
2023 C ed.
Practical Aspects of Declarative Languages - 26th International Symposium, PADL 2024, London, UK, January 15-16, 2024, Proceedings
PADL
Martin Gebser, Ilya Sergey
2023 J jnl
Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112).
Dagstuhl Reports
Swen Jacobs, Kenneth L. McMillan, Roopsha Samanta, Ilya Sergey
2022 B ed.
Programming Languages and Systems - 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings
APLAS
Ilya Sergey
2022 A ed.
Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings
ESOP
Ilya Sergey
2022 J jnl
Random testing of a higher-order blockchain language (experience report).
Proc. ACM Program. Lang.
Tram Hoang, Anton Trunov, Leonidas Lampropoulos, Ilya Sergey
2021 B conf
Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis.
VMCAI
Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin
2021 J jnl
Certifying the synthesis of heap-manipulating programs.
Proc. ACM Program. Lang.
Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey
2021 A* conf
Cyclic program synthesis.
PLDI
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey
2021 — conf
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper).
CAV (1)
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey
2021 J jnl
HIPPODROME: Data Race Repair using Static Analysis Summaries.
CoRR
Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey
2021 A* conf
Practical smart contract sharding with ownership and commutativity analysis.
PLDI
George Pîrlea, Amrit Kumar, Ilya Sergey
2021 J jnl
Protocol combinators for modeling, testing, and execution of distributed systems.
J. Funct. Program.
Kristoffer Just Arndal Andersen, Ilya Sergey
2020 J jnl
Certifying Certainty and Uncertainty in Approximate Membership Query Structures - Extended Version.
CoRR
Kiran Gopinathan, Ilya Sergey
2020 — conf
Certifying Certainty and Uncertainty in Approximate Membership Query Structures.
CAV (2)
Kiran Gopinathan, Ilya Sergey
2020 J jnl
Compiling a Higher-Order Smart Contract Language to LLVM.
CoRR
Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea, Amrit Kumar, Ilya Sergey
2020 J jnl
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers - Extended Version.
CoRR
Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey
2020 A conf
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers.
ESOP
Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey
2020 J jnl
QED at Large: A Survey of Engineering of Formally Verified Software.
CoRR
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
2019 J jnl
A true positives theorem for a static race detector.
Proc. ACM Program. Lang.
Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
2019 C conf
Distributed Protocol Combinators.
PADL
Kristoffer Just Arndal Andersen, Ilya Sergey
2019 A* conf
Engineering Distributed Systems that We Can Trust (and Also Run).
PODC
Ilya Sergey
2019 A conf
Exploiting the laws of order in smart contracts.
ISSTA
Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena
2019 J jnl
QED at Large: A Survey of Engineering of Formally Verified Software.
Found. Trends Program. Lang.
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
2019 C conf
Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis.
VECoS
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
2019 J jnl
Safer smart contract programming with Scilla.
Proc. ACM Program. Lang.
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, Ken Chan Guan Hao
2019 J jnl
Structuring the synthesis of heap-manipulating programs.
Proc. ACM Program. Lang.
Nadia Polikarpova, Ilya Sergey
2018 J jnl
A True Positives Theorem for a Static Race Detector - Extended Version.
CoRR
Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
2018 B conf
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode.
ATVA
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey
2018 J jnl
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode.
CoRR
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey
2018 J jnl
Exploiting The Laws of Order in Smart Contracts.
CoRR
Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena
2018 A conf
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale.
ACSAC
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor
2018 J jnl
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale.
CoRR
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor
2018 J jnl
GASTAP: A Gas Analyzer for Smart Contracts.
CoRR
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
2018 B conf
Mechanising blockchain consensus.
CPP
George Pîrlea, Ilya Sergey
2018 J jnl
Paxos Consensus, Deconstructed and Abstracted (Extended Version).
CoRR
Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey
2018 A conf
Paxos Consensus, Deconstructed and Abstracted.
ESOP
Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey
2018 J jnl
Programming and proving with distributed protocols.
Proc. ACM Program. Lang.
Ilya Sergey, James R. Wilcox, Zachary Tatlock
2018 J jnl
RacerD: compositional static race detection.
Proc. ACM Program. Lang.
Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
2018 J jnl
Scilla: a Smart Contract Intermediate-Level LAnguage.
CoRR
Ilya Sergey, Amrit Kumar, Aquinas Hobor
2018 J jnl
Structuring the Synthesis of Heap-Manipulating Programs.
CoRR
Nadia Polikarpova, Ilya Sergey
2018 — conf
Temporal Properties of Smart Contracts.
ISoLA (4)
Ilya Sergey, Amrit Kumar, Aquinas Hobor
2017 — conf
A Concurrent Perspective on Smart Contracts.
Financial Cryptography Workshops
Ilya Sergey, Aquinas Hobor
2017 J jnl
A Concurrent Perspective on Smart Contracts.
CoRR
Ilya Sergey, Aquinas Hobor
2017 J jnl
Concurrent Data Structures Linked in Time (Artifact).
Dagstuhl Artifacts Ser.
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2017 A conf
Concurrent Data Structures Linked in Time.
ECOOP
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2017 J jnl
Modular, higher order cardinality analysis in theory and practice.
J. Funct. Program.
Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones, Joachim Breitner
2017 — conf
Programming Language Abstractions for Modularly Verified Distributed Systems.
SNAPL
James R. Wilcox, Ilya Sergey, Zachary Tatlock
2016 J jnl
Concurrent Data Structures Linked in Time.
CoRR
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2016 A conf
Experience report: growing and shrinking polygons for random testing of computational geometry algorithms.
ICFP
Ilya Sergey
2016 A conf
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects.
OOPSLA
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
2016 J jnl
Operational Aspects of C/C++ Concurrency.
CoRR
Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski
2015 J jnl
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects.
CoRR
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
2015 A* conf
Mechanized verification of fine-grained concurrent programs.
PLDI
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2015 A conf
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.
ESOP
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2014 A conf
Communicating State Transition Systems for Fine-Grained Concurrent Resources.
ESOP
Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco
2014 C conf
Deriving interpretations of the gradually-typed lambda calculus.
PEPM
Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey
2014 A* conf
Modular, higher-order cardinality analysis in theory and practice.
POPL
Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones
2014 J jnl
Pushdown flow analysis with abstract garbage collection.
CoRR
Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn
2014 J jnl
Pushdown flow analysis with abstract garbage collection.
J. Funct. Program.
Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn
2014 J jnl
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.
CoRR
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
2013 C conf
Fixing idioms: a recursion primitive for applicative DSLs.
PEPM
Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens
2013 A* conf
Monadic abstract interpreters.
PLDI
Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens
2013 — ch.
Ownership Types: A Survey.
Aliasing in Object-Oriented Programming
Dave Clarke, Johan Östlund, Ilya Sergey, Tobias Wrigstad
2012 J jnl
A correspondence between type checking via reduction and type checking via evaluation.
Inf. Process. Lett.
Ilya Sergey, Dave Clarke
2012 B conf
Calculating Graph Algorithms for Dominance and Shortest Path.
MPC
Ilya Sergey, Jan Midtgaard, Dave Clarke
2012 A conf
Gradual Ownership Types.
ESOP
Ilya Sergey, Dave Clarke
2012 J jnl
Introspective Pushdown Analysis of Higher-Order Programs
CoRR
Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
2012 A conf
Introspective pushdown analysis of higher-order programs.
ICFP
Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn
2011 — conf
From type checking by recursive descent to type checking with an abstract machine.
LDTA
Ilya Sergey, Dave Clarke
2009 — conf
A semantics for context-oriented programming with layers.
COP@ECOOP
Dave Clarke, Ilya Sergey