Artem Khyzha

I currently work at Arm, where my mission is to extend the memory-model tools, that is, to model new features of the Arm architectures, study their impact on memory consistency and encode it in executable semantics.

This webpage snapshots my interest in researching semantics of persistent and multicore programming, as well as hardware security. Until recently, I was exploring those interests as a postdoctoral fellow at Tel Aviv University and a PhD student at IMDEA Software Institute. My PhD thesis was about specifying and verifying concurrent objects.

• Moshik Hershcovitch, Artem Khyzha, Daniel Waddington, and Adam Morrison
  Elastic Indexes: Dynamic Space vs Query Efficiency Tuning for In-Memory Database Indexing.
  EDBT'22: International Conference on Extending Database Technology. To appear.
  
  
• Artem Khyzha, Ori Lahav
  Abstraction for Crash-Resilient Objects
  ESOP'22: European Symposium on Programming. To appear.
  [arXiv Version]
  
  
• Artem Khyzha, Ori Lahav
  Taming x86-TSO Persistency
  POPL'21: Symposium on Principles of Programming Languages, 2021.
  [DOI] [Extended Version]
  
  
• Yotam Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
  Proving Highly-Concurrent Traversals Correct
  OOPSLA'20: International Conference on Object-Oriented Programming, Systems, Languages, and Applications.
  [DOI] [Extended Version]
  
  
• Jiyong Yu, Mengjia Yan, Artem Khyzha, Adam Morrison, Josep Torrellas, Christopher Fletcher
  Speculative Taint Tracking (STT): A Comprehensive Protection for Speculatively Accessed Data
  MICRO'19: International Symposium on Microarchitecture, 2019.
  [DOI] [Formal Analysis]
  
  
• Artem Khyzha, Hagit Attiya, Alexey Gotsman
  Privatization-safe Transactional Memories
  DISC'19: International Symposium on Distributed Computing.
  [DOI] [Extended version]
  
  
• Artem Khyzha, Hagit Attiya, Alexey Gotsman, Noam Rinetzky
  Safe Privatization for Transactional Memory
  PPoPP'18: Principles and Practice of Parallel Programming.
  [DOI] [Extended version]
  
  
• Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson
  Proving Linearizability Using Partial Orders
  ESOP'17: European Symposium on Programming
  [DOI] [Extended version]
  
  
• Artem Khyzha, Alexey Gotsman, Matthew Parkinson
  A Generic Logic for Proving Linearizability
  FM'16: International Symposium on Formal Methods
  [DOI] [Extended version]
  
  

My last name is a rare word for a hut in Ukrainian. Its romanization looks unusual, so maybe you want to click on this link and hear me pronouncing my full name. Otherwise, here is a brief pronunciation guide: the "k" in "kh" is effectively silent, and "zh" is not entirely unlike "j" in French or Portuguese.