Alexey Gotsman Assistant 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 tenure-track Assistant 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 software verfication, particularly, in developing reasoning techniques and automated verification tools for real-world concurrent systems software.

Research group

• Giovanni Bernardi, Postdoc

• Andrea Cerone, Postdoc

• Artem Khyzha, PhD student

I am looking for enthusiastic students to work with me on topics of mutual interest. If you're interested in doing an internship with me, send me an email.

Recent publications

• Alexey Gotsman and Hongseok Yang
  Composite replicated data types [PDF]
  ESOP'15: European Symposium on Programming, London, UK. To appear.
  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]

• Alexey Gotsman and Hongseok Yang
  Linearizability with ownership transfer [PDF]
  Logical Methods in Computer Science, 9(3:12), 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):452-514. 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, Montreal, Canada, pages 309-318. ACM, 2013.
  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, Rome, Italy, LNCS 7792, pages 249-269. Springer, 2013.
  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, Rome, Italy, pages 235-248. ACM, 2013.
  Extended version: Technical Report YCS-2012-479, University of York, 2012 [PDF]
  Twitter version: TinyTOCS, Vol. 2, 2013 [PDF]

• All publications

Funding

• I am 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: POPL'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

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

Selected talks

• Abstraction for Weakly Consistent Systems. Invited talk at WS-FMDS'13, affiliated with SEFM'13 [Slides]

• Understanding Eventual Consistency. Invited talk at REORDER/EC2, affiliated with CAV'13 [Slides]

• Consistency in Concurrent and Distributed Systems. Invited tutorial at POPL'13 [Slides]

Teaching

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