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 successfully transitioned to the doctorate part of my programme.

My research is mainly about modular verification of fine-grained concurrent software with a specific focus on proving linearizability and contextual refinement. I am also interested in design of scallable concurrent algorithms.



Publications

  • Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson
    Proving Linearizability Using Partial Orders
    ESOP: European Symposium on Programming, Uppsala, Sweden, 2017.
    [PDF] [arXiv*]
    * -- in the state of being updated from the submitted to final status

  • 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

  • Proving Linearizability Using Partial Orders [Slides]
    IMDEA Software Seminar Series, Madrid, Spain, November 2016
  • Proving Linearizability Using Partial Orders [Slides]
    Kent Concurrency Workshop, Canterbury, UK, July 2016
  • 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]
    Modelling and Verifying Parallel processes (MOVEP), Marseille, France, 2012