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 (Microsoft Research European PhD Scholarship)

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

Projects

Recent publications

• Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
  Safety of live transactions in transactional memory: TMS is necessary and sufficient
  DISC'14: International Symposium on Distributed Computing, Austin, TX, USA. To appear.

• Andrea Cerone, Alexey Gotsman, and Hongseok Yang
  Parameterised linearisability [PDF]
  ICALP'14: International Colloquium on Automata, Languages, and Programming, Copenhagen, Denmark. To appear.
  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

Activities

• Programme committees: ESOP'15, OPODIS'14, ESOP'14, VMCAI'14, ICALP'13, MFPS'12, SSV'11, FMICS'09

• Co-organiser: Workshop on Principles and Practice of Eventual Consistency, affiliated with EuroSys'14

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]