Publications

• Manuel Bravo, Gregory Chockler, Alexey Gotsman, Alejandro Naser-Pastoriza, and Christian Roldán
  Vertical atomic broadcast and passive replication [PDF]
  DISC'24: International Symposium on Distributed Computing
  Extended version available as arXiv:2408.08702 [PDF]

• Manuel Bravo, Gregory Chockler, and Alexey Gotsman
  Liveness and latency of Byzantine state-machine replication [PDF]
  Distributed Computing. Springer, 2024.
  Journal version of our DISC'22 paper.

• Fedor Ryabinin, Alexey Gotsman, and Pierre Sutra
  SwiftPaxos: Fast geo-replicated state machines [PDF] [Code]
  NSDI'24: Symposium on Networked Systems Design and Implementation

• Alejandro Naser-Pastoriza, Gregory Chockler, and Alexey Gotsman
  Fault-tolerant computing with unreliable channels [PDF]
  OPODIS'23: International Conference on Principles of Distributed Systems
  Extended version available as arXiv:2305.15150 [PDF]
  Best paper award

• Manuel Bravo, Gregory Chockler, and Alexey Gotsman
  Liveness and latency of Byzantine state-machine replication [PDF]
  DISC'22: International Symposium on Distributed Computing
  Extended version available as arXiv:2202.06679 [PDF]

• Manuel Bravo, Gregory Chockler, and Alexey Gotsman
  Making Byzantine consensus live [PDF]
  Distributed Computing, 35(6). Springer, 2022.
  Journal version of our DISC'20 paper.

• Joseph Izraelevitz, Gaukas Wang, Rhett Hanscom, Kayli Silvers, Tamara Silbergleit Lehman, Gregory Chockler and Alexey Gotsman
  Acuerdo: Fast atomic broadcast over RDMA [PDF]
  ICPP'22: International Conference on Parallel Processing

• Manuel Bravo, Alexey Gotsman, Borja de Régil, and Hengfeng Wei
  UniStore: A fault-tolerant marriage of causal and strong consistency [PDF]
  USENIX ATC'21: USENIX Annual Technical Conference
  Extended version available as arXiv:2106.00344 [PDF]

• Vitor Enes, Carlos Baquero, Alexey Gotsman, and Pierre Sutra
  Efficient replication via timestamp stability [PDF] [Code]
  EuroSys'21: European Conference on Computer Systems
  Extended version available as arXiv:2104.01142 [PDF]

• Gregory Chockler and Alexey Gotsman
  Multi-shot distributed transaction commit [PDF]
  Distributed Computing, 34(4). Springer, 2021.
  Journal version of our DISC'18 paper.

• Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski
  Specification and space complexity of collaborative text editing [PDF]
  Theoretical Computer Science, 855. Elsevier, 2021.
  Journal version of our PODC'16 paper.

• Manuel Bravo, Gregory Chockler, and Alexey Gotsman
  Making Byzantine consensus live [PDF]
  DISC'20: International Symposium on Distributed Computing
  Extended version available as arXiv:2008.04167 [PDF]

• Vitor Enes, Carlos Baquero, Tuanir França Rezende, Alexey Gotsman, Matthieu Perrin, and Pierre Sutra
  State-machine replication for planet-scale systems [PDF]
  EuroSys'20: European Conference on Computer Systems
  Extended version available as arXiv:2003.11789 [PDF]

• Artem Khyzha, Hagit Attiya and Alexey Gotsman
  Privatization-safe transactional memories [PDF]
  DISC'19: International Symposium on Distributed Computing
  Extended version available as arXiv:1908.03179 [PDF]

• Manuel Bravo and Alexey Gotsman
  Reconfigurable atomic transaction commit [PDF]
  PODC'19: Symposium on Principles of Distributed Computing
  Extended version available as arXiv:1906.01365 [PDF]

• Alexey Gotsman, Anatole Lefort and Gregory Chockler
  White-box atomic multicast [PDF] [Code]
  DSN'19: International Conference on Dependable Systems and Networks
  Extended version available as arXiv:1904.07171 [PDF]

• Andrea Cerone and Alexey Gotsman
  Analysing snapshot isolation [PDF]
  Journal of the ACM, 65(2). ACM, 2018.
  Journal version of our PODC'16 paper.

• Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
  Characterizing transactional memory consistency conditions using observational refinement [PDF]
  Journal of the ACM, 65(1). ACM, 2018.
  Journal version of our PODC'13 and DISC'14 papers.

• Álvaro García-Pérez and Alexey Gotsman
  Federated Byzantine quorum systems [PDF]
  OPODIS'18: International Conference on Principles of Distributed Systems
  Extended version available as arXiv:1811.03642 [PDF]

• Gregory Chockler and Alexey Gotsman
  Multi-shot distributed transaction commit [PDF]
  DISC'18: International Symposium on Distributed Computing
  Extended version available as arXiv:1808.00688 [PDF]
  Best paper award

• Artem Khyzha, Hagit Attiya, Alexey Gotsman, and Noam Rinetzky
  Safe privatization in transactional memory [PDF]
  PPoPP'18: Symposium on Principles and Practice of Parallel Programming
  Extended version available as arXiv:1801.04249 [PDF]
  

• Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, and Ilya Sergey
  Paxos consensus, deconstructed and abstracted [PDF]
  ESOP'18: European Symposium on Programming
  Extended version available as arXiv:1802.05969 [PDF]

• Mike Dodds, Mark Batty, and Alexey Gotsman
  Compositional verification of compiler optimisations on relaxed memory [PDF]
  ESOP'18: European Symposium on Programming
  Extended version available as arXiv:1802.05918 [PDF]

• Alexey Gotsman and Sebastian Burckhardt
  Consistency models with global operation sequencing and their composition [PDF]
  DISC'17: International Symposium on Distributed Computing
  Extended version available as arXiv:1707.09242 [PDF]
  

• Andrea Cerone, Alexey Gotsman, and Hongseok Yang
  Algebraic laws for weak consistency [PDF]
  CONCUR'17: International Conference on Concurrency Theory
  Extended version available as arXiv:1702.06028 [PDF]
  

• Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson
  Proving linearizability using partial orders [PDF]
  ESOP'17: European Symposium on Programming
  Extended version available as arXiv:1701.05463 [PDF]
  

• Andrea Cerone and Alexey Gotsman
  Analysing snapshot isolation [PDF]
  PODC'16: Symposium on Principles of Distributed Computing
  Extended version [PDF]
  Best paper award

• Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski
  Specification and complexity of collaborative text editing [PDF]
  PODC'16: Symposium on Principles of Distributed Computing
  Extended version [PDF]

• Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro
  'Cause I'm strong enough: reasoning about consistency choices in distributed systems [PDF]
  POPL'16: Symposium on Principles of Programming Languages
  Extended version [PDF]
  Tool paper [PDF]

• Artem Khyzha, Alexey Gotsman, and Matthew Parkinson
  A generic logic for proving linearizability [PDF]
  FM'16: International Symposium on Formal Methods
  Extended version available as arXiv:1609.01171 [PDF]
  

• Giovanni Bernardi and Alexey Gotsman
  Robustness against consistency models with atomic visibility [PDF]
  CONCUR'16: International Conference on Concurrency Theory
  Extended version [PDF]
  

• Andrea Cerone, Alexey Gotsman, and Hongseok Yang
  Transaction chopping for parallel snapshot isolation [PDF]
  DISC'15: International Symposium on Distributed Computing
  Extended version [PDF]

• Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman
  A framework for transactional consistency models with atomic visibility [PDF]
  CONCUR'15: International Conference on Concurrency Theory
  Extended version [PDF]

• Alexey Gotsman and Hongseok Yang
  Composite replicated data types [PDF]
  ESOP'15: European Symposium on Programming
  Extended version [PDF]

• Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
  Safety of live transactions in transactional memory: TMS is necessary and sufficient [PDF]
  DISC'14: International Symposium on Distributed Computing
  Extended version: Technical Report CS-2014-02, Technion, 2014 [PDF]

• Andrea Cerone, Alexey Gotsman, and Hongseok Yang
  Parameterised linearisability [PDF]
  ICALP'14: International Colloquium on Automata, Languages, and Programming
  Extended version [PDF]

• Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski
  Replicated data types: specification, verification, optimality [PDF]
  POPL'14: Symposium on Principles of Programming Languages
  Extended version [PDF]
  Preliminary version (with some additional material): Understanding eventual consistency, Microsoft Research Technical Report MSR-TR-2013-39 [PDF]

• Alexey Gotsman and Hongseok Yang
  Linearizability with ownership transfer [PDF]
  Logical Methods in Computer Science, 9(3), 2013.
  Journal version of our CONCUR'12 paper.

• Alexey Gotsman and Hongseok Yang
  Modular verification of preemptive OS kernels [PDF]
  Journal of Functional Programming, 23(4). Cambridge University Press, 2013.
  Journal version of our ICFP'11 paper. Electronic appendix [PDF]

• Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
  A programming language perspective on transactional memory consistency [PDF]
  PODC'13: Symposium on Principles of Distributed Computing
  Extended version: Technical Report CS-2013-04, Technion, 2013 [PDF]

• Alexey Gotsman, Noam Rinetzky, and Hongseok Yang
  Verifying concurrent memory reclamation algorithms with grace [PDF]
  ESOP'13: European Symposium on Programming
  Extended version: Technical Report 7/13, School of Computer Science, Tel-Aviv University [PDF]

• Mark Batty, Mike Dodds, and Alexey Gotsman
  Library abstraction for C/C++ concurrency [PDF]
  POPL'13: Symposium on Principles of Programming Languages
  Extended version: Technical Report YCS-2012-479, University of York, 2012 [PDF]

• Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang
  Show no weakness: sequentially consistent specifications of TSO libraries [PDF]
  DISC'12: International Symposium on Distributed Computing
  Extended version [PDF]

• Alexey Gotsman and Hongseok Yang
  Linearizability with ownership transfer [PDF]
  CONCUR'12: International Conference on Concurrency Theory
  Best paper award
  Extended version [PDF]

• Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang
  Concurrent library correctness on the TSO memory model [PDF]
  ESOP'12: European Symposium on Programming
  Extended version [PDF]

• Alexey Gotsman and Hongseok Yang
  Modular verification of preemptive OS kernels [PDF]
  ICFP'11: International Conference on Functional Programming
  Extended version [PDF]

• Alexey Gotsman and Hongseok Yang
  Liveness-preserving atomicity abstraction [PDF]
  ICALP'11: International Colloquium on Automata, Languages and Programming
  Extended version [PDF]

• Alexey Gotsman, Josh Berdine, and Byron Cook
  Precision and the conjunction rule in concurrent separation logic [PDF]
  MFPS'11: Conference on the Mathematical Foundations of Programming Semantics

• Alexey Gotsman
  Logics and analyses for concurrent heap-manipulating programs [PDF]
  Ph.D. dissertation. Available as Technical Report UCAM-CL-TR-758, University of Cambridge Computer Laboratory, 2009.
  EAPLS Best Dissertation Award. Runner-up prize in the BCS Distinguished Dissertation Competition.

• Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis
  Proving that non-blocking algorithms don't block [PDF]
  POPL'09: Symposium on Principles of Programming Languages

• Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv
  Local reasoning for storable locks and threads [PDF]
  APLAS'07: Asian Symposium on Programming Languages and Systems
  Extended version: Technical Report MSR-TR-2007-39, Microsoft Research, 2007 [PDF]

• Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly Sagiv
  Thread-modular shape analysis [PDF]
  PLDI'07: Conference on Programming Languages Design and Implementation

• Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Y. Vardi
  Proving that programs eventually do something good [PDF]
  POPL'07: Symposium on Principles of Programming Languages

• Alexey Gotsman, Josh Berdine, and Byron Cook
  Interprocedural shape analysis with separated heap abstractions [PDF]
  SAS'06: International Static Analysis Symposium

• Alexey Gotsman, Fabio Massacci, and Marco Pistore
  Towards an independent semantics and verification technology for the HLPSL specification language [PDF]
  ARSPA'05: Workshop on Automated Reasoning for Security Protocol Analysis