Travelled to:1 × Denmark
1 × Estonia
1 × France
1 × Japan
1 × Korea
1 × Switzerland
1 × United Kingdom
2 × Italy
3 × USA
Collaborated with:H.Yang B.Cook M.Dodds M.Batty J.Berdine S.Burckhardt M.J.Parkinson A.Cerone N.Rinetzky M.Zawirski M.Musuvathi V.Vafeiadis M.Sagiv A.Khyzha Á.García-Pérez Y.Meshman I.Sergey A.Podelski A.Rybalchenko M.Y.Vardi Carla Ferreira 0001 Mahsa Najafzadeh Marc Shapiro 0001
Talks about:abstract (4) concurr (3) memori (3) verif (3) prove (3) algorithm (2) composit (2) modular (2) librari (2) analysi (2)
Person: Alexey Gotsman
DBLP: Gotsman:Alexey
Contributed to:
2015
2014
20142013201320122011
20112009
20072007
2006201720182016Wrote 16 papers:
- ESOP-2015-GotsmanY #data type
- Composite Replicated Data Types (AG, HY), pp. 585–609.
- ICALP-v2-2014-CeroneGY
- Parameterised Linearisability (AC, AG, HY), pp. 98–109.
- POPL-2014-BurckhardtGYZ #data type #specification #verification
- Replicated data types: specification, verification, optimality (SB, AG, HY, MZ), pp. 271–284.
- ESOP-2013-GotsmanRY #algorithm #concurrent #memory management #verification
- Verifying Concurrent Memory Reclamation Algorithms with Grace (AG, NR, HY), pp. 249–269.
- POPL-2013-BattyDG #abstraction #c #c++ #concurrent #library
- Library abstraction for C/C++ concurrency (MB, MD, AG), pp. 235–248.
- ESOP-2012-BurckhardtGMY #concurrent #correctness #library #memory management
- Concurrent Library Correctness on the TSO Memory Model (SB, AG, MM, HY), pp. 87–107.
- ICALP-v2-2011-GotsmanY #abstraction
- Liveness-Preserving Atomicity Abstraction (AG, HY), pp. 453–465.
- ICFP-2011-GotsmanY #composition #kernel #verification
- Modular verification of preemptive OS kernels (AG, HY), pp. 404–417.
- POPL-2009-GotsmanCPV #algorithm #proving
- Proving that non-blocking algorithms don’t block (AG, BC, MJP, VV), pp. 16–28.
- PLDI-2007-GotsmanBCS #analysis #thread
- Thread-modular shape analysis (AG, JB, BC, MS), pp. 266–277.
- POPL-2007-CookGPRV #proving #source code
- Proving that programs eventually do something good (BC, AG, AP, AR, MYV), pp. 265–276.
- SAS-2006-GotsmanBC #abstraction #analysis #interprocedural
- Interprocedural Shape Analysis with Separated Heap Abstractions (AG, JB, BC), pp. 240–260.
- ESOP-2017-KhyzhaDGP #partial order #proving #using
- Proving Linearizability Using Partial Orders (AK, MD, AG, MJP), pp. 639–667.
- ESOP-2018-DoddsBG #compilation #composition #memory management #optimisation #verification
- Compositional Verification of Compiler Optimisations on Relaxed Memory (MD, MB, AG), pp. 1027–1055.
- ESOP-2018-Garcia-PerezGMS
- Paxos Consensus, Deconstructed and Abstracted (ÁGP, AG, YM, IS), pp. 912–939.
- POPL-2016-GotsmanYFNS #consistency #distributed #reasoning
- 'Cause I'm strong enough: reasoning about consistency choices in distributed systems (AG, HY, CF0, MN, MS0), pp. 371–384.