Artem Khyzha


I am a postdoctoral fellow at Tel Aviv University, where I work on formal foundations of hardware (weak) memory concurrency, persistency and hardware security. My ongoing research efforts are primarily concentrated on two topics:

  • modelling CPU microarchitecture and security properties for speculative execution;
  • studying correctness guarantees for crash-resilient data structures and language-level support for persistent programming.

Previously, I obtained my PhD at IMDEA Software Institute. I defended my PhD thesis in July 2018. Back then I worked on developing reasoning principles and proof methods for verifying consistency of concurrent data structures and transactional memory systems.


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