Ilya Sergey

According to our database, Ilya Sergey authored at least 63 papers between 2009 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Small Scale Reflection for the Working Lean User.

Vladimir Gladshtein, George Pîrlea, Ilya Sergey

CoRR, 2024

Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic.

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Adventure of a Lifetime: Extract Method Refactoring for Rust.

Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey

Proc. ACM Program. Lang., October, 2023

Hippodrome: Data Race Repair Using Static Analysis Summaries.

Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey

ACM Trans. Softw. Eng. Methodol., April, 2023

Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112).

Swen Jacobs, Kenneth McMillan, Roopsha Samanta, Ilya Sergey

Dagstuhl Reports, March, 2023

Mostly Automated Proof Repair for Verified Libraries.

Kiran Gopinathan, Mayank Keoliya, Ilya Sergey

Proc. ACM Program. Lang., 2023

Leveraging Rust Types for Program Synthesis.

Jonás Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey

Proc. ACM Program. Lang., 2023

Distributed System Fuzzing.

Ruijie Meng, George Pîrlea, Abhik Roychoudhury, Ilya Sergey

CoRR, 2023

Greybox Fuzzing of Distributed Systems.

Ruijie Meng, George Pîrlea, Abhik Roychoudhury, Ilya Sergey

Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

2022

Random testing of a higher-order blockchain language (experience report).

Tram Hoang, Anton Trunov, Leonidas Lampropoulos, Ilya Sergey

Proc. ACM Program. Lang., 2022

2021

Certifying the synthesis of heap-manipulating programs.

Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey

Proc. ACM Program. Lang., 2021

Protocol combinators for modeling, testing, and execution of distributed systems.

Kristoffer Just Arndal Andersen, Ilya Sergey

J. Funct. Program., 2021

Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis.

Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Practical smart contract sharding with ownership and commutativity analysis.

George Pîrlea, Amrit Kumar, Ilya Sergey

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Cyclic program synthesis.

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper).

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Compiling a Higher-Order Smart Contract Language to LLVM.

Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea, Amrit Kumar, Ilya Sergey

CoRR, 2020

Certifying Certainty and Uncertainty in Approximate Membership Query Structures - Extended Version.

Kiran Gopinathan, Ilya Sergey

CoRR, 2020

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers - Extended Version.

Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey

CoRR, 2020

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers.

Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey

Proceedings of the Programming Languages and Systems, 2020

Certifying Certainty and Uncertainty in Approximate Membership Query Structures.

Kiran Gopinathan, Ilya Sergey

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Safer smart contract programming with Scilla.

Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, Ken Chan Guan Hao

Proc. ACM Program. Lang., 2019

Structuring the synthesis of heap-manipulating programs.

Nadia Polikarpova, Ilya Sergey

Proc. ACM Program. Lang., 2019

A true positives theorem for a static race detector.

Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey

Proc. ACM Program. Lang., 2019

QED at Large: A Survey of Engineering of Formally Verified Software.

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock

Found. Trends Program. Lang., 2019

Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis.

Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey

Proceedings of the Verification and Evaluation of Computer and Communication Systems, 2019

Engineering Distributed Systems that We Can Trust (and Also Run).

Ilya Sergey

Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, 2019

Distributed Protocol Combinators.

Kristoffer Just Arndal Andersen, Ilya Sergey

Proceedings of the Practical Aspects of Declarative Languages, 2019

Exploiting the laws of order in smart contracts.

Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena

Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2019

2018

Programming and proving with distributed protocols.

Ilya Sergey, James R. Wilcox, Zachary Tatlock

Proc. ACM Program. Lang., 2018

RacerD: compositional static race detection.

Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey

Proc. ACM Program. Lang., 2018

GASTAP: A Gas Analyzer for Smart Contracts.

Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey

CoRR, 2018

A True Positives Theorem for a Static Race Detector - Extended Version.

Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey

CoRR, 2018

Paxos Consensus, Deconstructed and Abstracted (Extended Version).

Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey

CoRR, 2018

Scilla: a Smart Contract Intermediate-Level LAnguage.

Ilya Sergey, Amrit Kumar, Aquinas Hobor

CoRR, 2018

Temporal Properties of Smart Contracts.

Ilya Sergey, Amrit Kumar, Aquinas Hobor

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018

Paxos Consensus, Deconstructed and Abstracted.

Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey

Proceedings of the Programming Languages and Systems, 2018

Mechanising blockchain consensus.

George Pîrlea, Ilya Sergey

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode.

Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey

Proceedings of the Automated Technology for Verification and Analysis, 2018

Finding The Greedy, Prodigal, and Suicidal Contracts at Scale.

Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor

Proceedings of the 34th Annual Computer Security Applications Conference, 2018

2017

Modular, higher order cardinality analysis in theory and practice.

Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones, Joachim Breitner

J. Funct. Program., 2017

Concurrent Data Structures Linked in Time (Artifact).

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee

Dagstuhl Artifacts Ser., 2017

Programming Language Abstractions for Modularly Verified Distributed Systems.

James R. Wilcox, Ilya Sergey, Zachary Tatlock

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

A Concurrent Perspective on Smart Contracts.

Ilya Sergey, Aquinas Hobor

Proceedings of the Financial Cryptography and Data Security, 2017

Concurrent Data Structures Linked in Time.

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

2016

Operational Aspects of C/C++ Concurrency.

Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski

CoRR, 2016

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects.

Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

Experience report: growing and shrinking polygons for random testing of computational geometry algorithms.

Ilya Sergey

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015

Mechanized verification of fine-grained concurrent programs.

Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.

Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee

Proceedings of the Programming Languages and Systems, 2015

2014

Pushdown flow analysis with abstract garbage collection.

J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn

J. Funct. Program., 2014

Modular, higher-order cardinality analysis in theory and practice.

Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Deriving interpretations of the gradually-typed lambda calculus.

Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey

Proceedings of the ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation, 2014

Communicating State Transition Systems for Fine-Grained Concurrent Resources.

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco

Proceedings of the Programming Languages and Systems, 2014

2013

Ownership Types: A Survey.

Dave Clarke, Johan Östlund, Ilya Sergey, Tobias Wrigstad

Proceedings of the Aliasing in Object-Oriented Programming. Types, 2013

Monadic abstract interpreters.

Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Fixing idioms: a recursion primitive for applicative DSLs.

Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens

Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, 2013

2012

A correspondence between type checking via reduction and type checking via evaluation.

Ilya Sergey, Dave Clarke

Inf. Process. Lett., 2012

Calculating Graph Algorithms for Dominance and Shortest Path.

Ilya Sergey, Jan Midtgaard, Dave Clarke

Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Introspective pushdown analysis of higher-order programs.

Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

Gradual Ownership Types.

Ilya Sergey, Dave Clarke

Proceedings of the Programming Languages and Systems, 2012

2011

From type checking by recursive descent to type checking with an abstract machine.

Ilya Sergey, Dave Clarke

Proceedings of the Language Descriptions, Tools and Applications, 2011

2009

A semantics for context-oriented programming with layers.

Dave Clarke, Ilya Sergey

Proceedings of the International Workshop on Context-Oriented Programming, 2009