Alexey Gotsman Associate Research Professor IMDEA Software Institute Campus Montegancedo s/n 28223-Pozuelo de Alarcón, Madrid, Spain Tel.: +34-91-101-2202 ext 4136 Fax: +34-91-101-1358 @ Email: Alexey.Gotsman imdea.org

I am a tenured Associate Research Professor at the IMDEA Software Institute. Before joining IMDEA, I was a postdoctoral fellow at the University of Cambridge, where I also got my Ph.D. My research interests are in methods and tools for developing correct concurrent and distributed software.

Research group

• Álvaro García Pérez, Postdoc

• Yuri Meshman, Postdoc

• Matthieu Perrin, Postdoc

• Artem Khyzha, PhD student

• Borja de Régil, Intern

• Vitor Enes, Intern

I have multiple PhD and postdoc positions available, funded by an ERC grant. If you're interested, drop me an email.

Alumni:

• Giovanni Bernardi (postdoc), now faculty at University of Paris 7

• Andrea Cerone (postdoc), now postdoc at Imperial College London

Recent publications

• Alexey Gotsman and Sebastian Burckhardt
  Consistency models with global operation sequencing and their composition
  DISC'17: International Symposium on Distributed Computing, Vienna, Austria. To appear.

• Andrea Cerone, Alexey Gotsman, and Hongseok Yang
  Algebraic laws for weak consistency
  CONCUR'17: International Conference on Concurrency Theory, Berlin, Germany. To appear.

• Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson
  Proving linearizability using partial orders [PDF]
  ESOP'17: European Symposium on Programming, Uppsala, Sweden, LNCS 10201, pages 639-667. Springer, 2017.
  Extended version available as arXiv:1701.05463 [PDF]
  

• Artem Khyzha, Alexey Gotsman, and Matthew Parkinson
  A generic logic for proving linearizability [PDF]
  FM'16: International Symposium on Formal Methods, Limassol, Cyprus, LNCS 9995, pages 426-443. Springer, 2016.
  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, Quebec City, Canada, LIPICS 59, pages 7:1-7:15, 2016.
  Extended version [PDF]
  

• Andrea Cerone and Alexey Gotsman
  Analysing snapshot isolation [PDF]
  PODC'16: Symposium on Principles of Distributed Computing, Chicago, IL, USA, pages 55-64. ACM, 2016.
  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, Chicago, IL, USA, pages 259-268. ACM, 2016.
  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, St. Petersburg, FL, USA, pages 371-384. ACM, 2016.
  Extended version [PDF]
  Tool demo [Video], Tool demo [PDF]

• Andrea Cerone, Alexey Gotsman, and Hongseok Yang
  Transaction chopping for parallel snapshot isolation [PDF]
  DISC'15: International Symposium on Distributed Computing, Tokyo, Japan, LNCS 9363, pages 388-404. Springer, 2015.
  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, Madrid, Spain, LIPICS 42, pages 58-71, 2015.
  Extended version [PDF]

• Alexey Gotsman and Hongseok Yang
  Composite replicated data types [PDF]
  ESOP'15: European Symposium on Programming, London, UK, LNCS 9032, pages 585-609. Springer, 2015.
  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, Austin, TX, USA, LNCS 8784, pages 376-390. Springer, 2014.
  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, Copenhagen, Denmark, LNCS 8573, pages 98-109. Springer, 2014.
  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, San Diego, CA, USA, pages 271-284. ACM, 2014.
  Extended version [PDF]
  Preliminary version (with some additional material): Understanding eventual consistency, Microsoft Research Technical Report MSR-TR-2013-39 [PDF]

• All publications

Funding

• ERC Starting Grant "RACCOON: A Rigorous Approach to Consistency in Cloud Databases"

• Ramón y Cajal Fellowship

• I was the coordinator of the EU project ADVENT, funded through the FP7 FET Young Explorers scheme

• Microsoft Research European PhD Scholarship, held by Artem Khyzha

• Microsoft Research Software Engineering Innovation Foundation Award (SEIF)

Activities

• Programme committees: PODC'18, ICALP'18, PLDI'17 (ERC), ESOP'17, PMLDC'17, TRANSACT'17, CONCUR'16, POPL'16, PMLDC'16, ESOP'15, APLAS'15, ACSD'15, PLACES'15, OPODIS'14, ESOP'14, VMCAI'14, PaPEC'14, ICALP'13, MFPS'12, SSV'11, FMICS'09

• Co-chair: Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC) 2017, affiliated with EuroSys

• Steering committee: Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC), affiliated with EuroSys

• Co-organiser: Dagstuhl Seminar "Data Consistency in Distributed Systems: Algorithms, Programs, and Databases"

Teaching

• Separation Logics and Applications, ENS Lyon Winter School, 2011 [Slides]