Artem Khyzha

Hello

I am a PhD student at IMDEA Software Institute under supervision of Alexey Gotsman. I joined the institute in September 2012, when I started a combined Master/PhD programme offered by Technical University of Madrid and IMDEA. After defending my Master thesis in July 2014, I started the doctorate part of my programme.

My research is mainly about modular verification of fine-grained concurrent software. I am also interested in design of scalable concurrent algorithms and software transactional memory.



Publications

  • Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson
    Proving Linearizability Using Partial Orders
    ESOP: European Symposium on Programming, Uppsala, Sweden, 2017.
    [PDF] [arXiv]

  • Artem Khyzha, Alexey Gotsman, Matthew Parkinson
    A Generic Logic for Proving Linearizability
    FM: International Symposium on Formal Methods, Limassol, Cyprus, 2016
    Extended version: [PDF] [arXiv]

  • Artem Khyzha
    Concurrent library abstraction without information hiding [PDF]
    Master thesis, Technical University of Madrid, 2014.

  • Artem Khyzha, Alexey Gotsman
    Compositional reasoning about concurrent libraries on the axiomatic TSO memory model
    Winter School on Modelling and Verifying Parallel Processes, Marseille, France, 2012.
    Extended abstract: [PDF]

  • Artem Khyzha, Pavel Parizek, Corina S. Pasareanu
    Abstract Pathfinder [PDF]
    The Java Pathfinder Workshop, Cary, North Carolina, USA, 2012.

Talks

  • Programming Language Perspective on Correctness of Software Transactional Memory
    SPTCC'17: The Summer Schoool on Practice and Theory of Concurrent Computing,
    St. Petersburg, Russia, July 2017
  • Proving Linearizability Using Partial Orders
    ESOP'17: European Symposium on Programming, Uppsala, Sweden, April 2017 [Slides]
    IMDEA Software Seminar Series, Madrid, Spain, November 2016 [Slides]
    Kent Concurrency Workshop, Canterbury, UK, July 2016 [Slides]
  • Relational Views Framework for Proving Linearizability [Slides]
    Imperial Concurrency Workshop, London, UK, July 2015
  • Concurrent library abstraction without information hiding [Slides]
    Master thesis defense, UPM, Madrid, Spain, 2014
  • Compositional reasoning about concurrent libraries on the axiomatic TSO memory model [Slides]
    MOVEP'12: The Winter School on Modelling and Verifying Parallel processes, Marseille, France, 2012