Publications

2016

• Analysing snapshot isolation
  Andrea Cerone and Alexey Gotsman
  PODC'16: Symposium on Principles of Distributed Computing, Chicago, IL, USA. To appear.
  Best paper award


• Specification and complexity of collaborative text editing
  Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski
  PODC'16: Symposium on Principles of Distributed Computing, Chicago, IL, USA. To appear.


• From Shape Analysis to Termination Analysis in Linear Time
  Roman Manevich, Boris Dogadov, and Noam Rinetzky.
  CAV 2016: CAV'16: Conference on Computer Aided Verification, Toronto, Ontario, Canada, July 2016. (To appear)


• Category theory in Coq 8.5
  Amin Timany and Bart Jacobs.
  FSCD 2016: 1st International Conference on Formal Structures for Computation and Deduction, Porto, Portugal. Dagstuhl LIPICS, June 2016.


• Validating optimizations of concurrent C/C++ programs
  Soham Chakraborty and Viktor Vafeiadis.
  CGO 2016: Symposium on Code Generation and Optimization, Barcelona, Spain. ACM, January 2016.
  [Paper] [Project page]


• Taming release-acquire consistency
  Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis.
  POPL 2016: Symposium on Principles of Programming Languages, St. Petersburg, FL, USA. ACM, January 2016.
  [Paper] [Project page]


• Lightweight verification of separate compilation
  Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis.
  POPL 2016: Symposium on Principles of Programming Languages, St. Petersburg, FL, USA. ACM, January 2016.
  [Paper] [Project page]


• 'Cause I'm strong enough: reasoning about consistency choices in distributed systems
  Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro
  POPL 2016: Symposium on Principles of Programming Languages, St. Petersburg, FL, USA. ACM, January 2016.
  [Paper]


• The CISE Tool: Proving Weakly-Consistent Applications Correct
  Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira, and Marc Shapiro.
  PAPOC 2016: Workshop on Principles and Practice of Consistency for Distributed Data, London, UK, April 2016.
  [Paper] [Tool Demo - Video]


• A program logic for C11 memory fences
  Marko Doko and Viktor Vafeiadis.
  VMCAI 2016: 17th International Conference on Verification, Model Checking, and Abstract Interpretation, St. Petersburg, FL, USA. Springer, January 2016.
  [Paper] [Project page]


• Property Directed Abstract Interpretation
  Noam Rinetzky and Sharon Shoham
  VMCAI'16: International Conference on Verification, Model Checking, and Abstract Interpretation. January 17-19, 2016, St. Petersburg, Florida, United States. [pdf]
  Best paper award

2015

• First steps towards cumulative inductive types in CIC
  Amin Timany and Bart Jacobs
  ICTAC 2015: International Colloquium on Theoretical Aspects of Computing, Cali, Colombia.
  [Paper]


• Transaction chopping for parallel snapshot isolation
  Andrea Cerone, Alexey Gotsman, and Hongseok Yang
  DISC 2015: International Symposium on Distributed Computing, Tokyo, Japan.
  [Paper]


• Asynchronous liquid separation types
  Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis.
  ECOOP 2015: 29th European Conference on Object-Oriented Programming, Prague, Czech Republic, LIPICS, 2015
  [Paper]


• Modularity in Lattices: A Case Study on the Correspondence between Top-Down and Bottom-Up Analysis
  Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, and Hongseok Yang
  SAS'15: 22nd International Static Analysis Symposium, Saint-Malo, France, September 9-11, 2015. [pdf]


• Pattern-based Synthesis of Synchronization for the C++ Memory Model
  Yuri Meshman, Noam Rinetzky, and Eran Yahav
  FMCAD'15: Formal Methods in Computer-Aided Design, September 27-30, 2015, Austin, Texas, USA [pdf]


• Property-Directed Inference of Universal Invariants or Proving Their Absence
  Alexander Karbyshev, Nikolaj Bjorner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham
  CAV'15: 27th International Conference on Computer Aided Verification, July 18-24, 2015, San Francisco, California. [pdf]


• Pilsner: A compositionally verified compiler for a higher-order imperative language
  Georg Neis, Georg Neis, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis.
  ICFP 2015: ACM SIGPLAN International Conference on Functional Programming, Vancouver, Canada, ACM, 2015. [Paper] [Project page]


• Rely/Guarantee Reasoning for Asynchronous Programs.
  Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis.
  CONCUR 2015: International Conference on Concurrency Theory, Madrid, Spain, LIPICS, 2015.
  [Paper]


• A framework for transactional consistency models with atomic visibility.
  Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman.
  CONCUR 2015: International Conference on Concurrency Theory, Madrid, Spain, LIPICS, 2015.
  [Paper]


• Owicki-Gries reasoning for weak memory models.
  Ori Lahav and Viktor Vafeiadis.
  ICALP 2015, Track B: 42nd International Colloquium on Automata, Languages, and Programming. Springer, July 2015
  [Paper] [Project page]


• Provably live exception handling.
  Bart Jacobs.
  FTfJP 2015: 17th Workshop on Formal Techniques for Java-like Programs. ACM Digital Library, July 2015
  [Paper]


• Modular termination verification.
  Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper.
  ECOOP 2015: 29th European Conference on Object-Oriented Programming. Dagstuhl LIPICS, July 2015
  [Paper]


• Verifying read-copy-update in a logic for weak memory.
  Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis.
  PLDI 2015: Symposium on Programming Language Design and Implementation. ACM, June 2015
  [Paper] [Project page]


• A formal C memory model supporting integer-pointer casts.
  Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis.
  PLDI 2015: Symposium on Programming Language Design and Implementation. ACM, June 2015
  [Paper] [Project page]


• Aspect-oriented linearizability proofs.
  Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
  Logical Methods in Computer Science 11(1:20), March 2015
  [Paper]


• Composite replicated data types
  Alexey Gotsman and Hongseok Yang
  ESOP 2015: European Symposium on Programming, London, UK, 2015.
  [PDF]


• Sound, modular and compositional verification of the input/output behavior of programs
  Willem Penninckx, Bart Jacobs, and Frank Piessens
  ESOP'15: European Symposium on Programming, London, UK, 2015.
  [PDF]


• Common compiler optimisations are invalid in the C11 memory model and what we can do about it.
  Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli.
  POPL 2015: Symposium on Principles of Programming Languages, Mumbai, India. ACM, 2015.
  [PDF] [Project page]


• Sound modular verification of C code executing in an unverified context
  Pieter Agten, Bart Jacobs, and Frank Piessens
  POPL 2015: Symposium on Principles of Programming Languages, Mumbai, India. ACM, 2015.
  [PDF]


• Verifying lock-freedom easily and automatically
  Xiao Jia, Wei Li, and Viktor Vafeiadis.
  CPP 2015: The 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, Mumbai, India. ACM, 2015.
  [PDF] [Project page]


• Modular verification of concurrency-aware linearizability
  Nir Hemed, Noam Rinetzky, and Viktor Vafeiadis.
  DISC 2015: International Symposium on Distributed Computing, Tokyo, Japan, 2015.
  [PDF]

2014

• GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation
  Aaron Turon, Viktor Vafeiadis, and Derek Dreyer
  OOPSLA 2014: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, Portland, USA. ACM, 2014.
  [PDF] [Project page]


• Safety of live transactions in transactional memory: TMS is necessary and sufficient
  Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
  DISC 2014: International Symposium on Distributed Computing, Austin, TX, USA, LNCS 8784, pages 376-390. Springer, 2014.
  [PDF] [Extended version, PDF]


• Brief Announcement: Concurrency-Aware Linearizability
  Nir Hemed and Noam Rinetzky
  PODC 2014: ACM Symposium on Principles of Distributed Computing, ACM, 2014.
  [PDF]


• Parameterised linearisability
  Andrea Cerone, Alexey Gotsman, and Hongseok Yang
  ICALP 2014: International Colloquium on Automata, Languages, and Programming, Copenhagen, Denmark, LNCS 8573, pages 98-109. Springer, 2014.
  [PDF] [Extended version, PDF]


• Replicated data types: specification, verification, optimality
  Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski
  POPL 2014: Symposium on Principles of Programming Languages, San Diego, CA, USA, pages 271-284. ACM, 2014.
  [PDF] [Extended version, PDF]


• A logical step forward in parametric bisimulations
  Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis
  Technical Report MPI-SWS-2014-003. Max Planck Institute for Software Systems (MPI-SWS), January 2014
  [PDF]

2013

• Relaxed separation logic: A program logic for C11 concurrency
  Viktor Vafeiadis and Chinmay Narayan
  OOPSLA 2013: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, Indianapolis, USA. ACM, 2013.
  [PDF] [Project page] [Slides (PDF)] [Tutorial slides (PDF)]


• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
  Aaron Turon, Derek Dreyer, Lars Birkedal
  ICFP 2013: ACM SIGPLAN International Conference on Functional Programming, Boston, USA. ACM, 2013.
  [PDF]


• Aspect-oriented linearizability proofs
  Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
  CONCUR 2013: Concurrency Theory, Buenos Aires, Argentina. LNCS, vol. 8052, pages 242-256. Springer, 2013.
  [PDF]


• Linearizability with ownership transfer
  Alexey Gotsman and Hongseok Yang
  Logical Methods in Computer Science, 9(3:12), 2013.
  [PDF]


• Modular verification of preemptive OS kernels
  Alexey Gotsman and Hongseok Yang
  Journal of Functional Programming. 23(4):452-514. Cambridge University Press, 2013.
  [PDF] [Appendix, PDF]


• C/C++ causal cycles confound compositionality
  Mike Dodds, Mark Batty, and Alexey Gotsman
  Tiny Transactions on Computer Science (TinyToCS), Vol. 2, 2013.
  [PDF]


• A programming language approach to fault tolerance for fork-join parallelism
  Mustafa Zengin and Viktor Vafeiadis
  TASE'13: The 7th International Symposium on Theoretical Aspects of Software Engineering, Birmingham, UK. IEEE, 2013.
  [PDF]


• A programming language perspective on transactional memory consistency
  Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
  PODC'13: Symposium on Principles of Distributed Computing, Montreal, Canada, pages 309-318. ACM, 2013.
  [PDF] [Extended version, PDF]


• Tightfit: Adaptive Parallelization with Foresight
  Omer Tripp and Noam Rinetzky
  ESEC/FSE'13: Conference on the Foundations of Software Engineerinq. Saint Petersburg, Russia, pages 169-179. ACM, 2013.
  [PDF]


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


• Verifying concurrent memory reclamation algorithms with grace
  Alexey Gotsman, Noam Rinetzky, and Hongseok Yang
  ESOP'13: European Symposium on Programming, Rome, Italy, LNCS 7792, pages 249-269. Springer, 2013.
  [PDF] [Extended version, PDF]


• Library abstraction for C/C++ concurrency
  Mark Batty, Mike Dodds, and Alexey Gotsman
  POPL'13: Symposium on Principles of Programming Languages, Rome, Italy, pages 235-248. ACM, 2013.
  [PDF] [Extended version, PDF]


• Modular Lattices for Compositional Interprocedural Analysis
  Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, and Hongseok Yang
  School of Computer Science, Tel Aviv University TR-103/13, 2013.
  [PDF]