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.

Projects

Publications

• Sebastian Burckhardt, Alexey Gotsman, and Hongseok Yang
  Understanding eventual consistency
  Microsoft Research Technical Report MSR-TR-2013-39 [PDF]

• Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
  A programming language perspective on transactional memory consistency
  PODC'13: Symposium on Principles of Distributed Computing, Montreal, Canada. ACM, 2013. To appear.

• 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 [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 [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, Salvador, Bahia, Brazil, LNCS 7611, pages 31-45. Springer, 2012.
  Extended version [PDF]

• Alexey Gotsman and Hongseok Yang
  Linearizability with ownership transfer [PDF]
  CONCUR'12: International Conference on Concurrency Theory, Newcastle upon Tyne, UK, LNCS 7454, pages 256-271. Springer, 2012.
  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, Tallinn, Estonia, LNCS 7211, pages 87-107. Springer, 2012.
  Extended version [PDF]

• Alexey Gotsman and Hongseok Yang
  Modular verification of preemptive OS kernels [PDF]
  ICFP'11: International Conference on Functional Programming, Tokyo, Japan, pages 404-417. ACM, 2011.
  Extended version [PDF]

• Alexey Gotsman and Hongseok Yang
  Liveness-preserving atomicity abstraction [PDF]
  ICALP'11: International Colloquium on Automata, Languages and Programming, Zurich, Switzerland, LNCS 6756, pages 453-465. Springer, 2011.
  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, Pittsburgh, PA, USA, ENTCS 276:171-190. Elsevier, 2011.

• 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, Savannah, GA, USA, pages 16-28. ACM, 2009.

• 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, Singapore, LNCS 4807, pages 19-37. Springer, 2007.
  Extended version appears as Microsoft Research Technical Report MSR-TR-2007-39, 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, San Diego, CA, USA, pages 266-277. ACM, 2007.

• 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, Nice, France, pages 265-276. ACM, 2007.

• Alexey Gotsman, Josh Berdine, and Byron Cook
  Interprocedural shape analysis with separated heap abstractions [PDF]
  SAS'06: International Static Analysis Symposium, Seoul, Korea, LNCS 4134, pages 240-260. Springer, 2006.

• 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, Lisbon, Portugal, ENTCS 135(1):59-77. Elsevier, 2005.

PhD students

• Artem Khyzha (Microsoft Research European PhD Scholarship).

Programme committees

• ESOP'14: European Symposium on Programming, Grenoble, France, April 7-11, 2014.

• ICALP'13: International Colloquium on Automata, Languages and Programming, Riga, Latvia, July 8-12, 2013.

• MFPS'12: Conference on the Mathematical Foundations of Programming Semantics, Bath, UK, June 5-10, 2012.

• SSV'11: Workshop on Systems Software Verification, Nijmegen, The Netherlands, August 26-27, 2011.

• FMICS'09: Workshop on Formal Methods for Industrial Critical Systems, Eindhoven, The Netherlands, November 2-3, 2009.

Teaching

• Tutorial on Consistency in Concurrent and Distributed Systems at POPL'13, January 21, 2013. [Slides]

• Separation Logics and Applications, ENS Lyon Winter School, January 31 - February 4, 2011. [Slides]