Alexey Gotsman University of Cambridge, Computer Laboratory William Gates Building, 15 JJ Thomson Avenue Cambridge CB3 0FD, UK Tel.: +44 1223 763575 Fax: +44 1223 334678 @ Email: Alexey.Gotsman cl.cam.ac.uk

I am a Ph.D. student in the Automated Reasoning Group supervised by Mike Gordon and Byron Cook. My research interests are in the areas of formal verification and programming languages, including program analysis, program logics, and software model checking.

Publications

• 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.

• 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 [PDF], April 2007 (revised September 2007).

• 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.

Programme committees

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

Teaching

• Concurrent and Distributed Systems, 2009/2010
• Optimising Compilers, 2009/2010
• Semantics of Programming Languages, 2008/2009
• Types, 2008/2009
• Specification and Verification II, 2007/2008
• Denotational Semantics, 2007/2008
• Foundations of Functional Programming, 2006/2007