cv

Basics

Name Egor Namakonov
Email e.namakonov@cs.au.dk
Url https://fresheed.github.io
About PhD student working on formal verification of concurrent programs

Education

  • Sep 2022 - Present

    Aarhus, Denmark

    PhD, Aarhus University
    Computer Science
  • Sep 2018 - Jul 2020

    St. Petersburg, Russia

    Master, St Petersburg University
    Computer Science
  • Sep 2013 - Jul 2017

    St. Petersburg, Russia

    Bachelor, Peter the Great St. Petersburg Polytechnic University
    Software Engineering

Industrial experience

  • Jul 2019 - Aug 2022

    St. Petersburg, Russia

    Intern and junior researcher, JetBrains Research
    Weak memory research, teaching
  • Nov 2015 - Jul 2018

    St. Petersburg, Russia

    Intern and DevOps engineer , OpenWay Group
    Continuous Integration, internal Python development, VM administration

Teaching

Volunteer

  • Jun 2022 - May 2024

    Remote

    Software engineer, OVD-Info
    Python chatbots development, CI
  • Jun 2022 - Nov 2022

    Remote

    Software engineer, Helping to Leave
    DSL-based chatbots development, JavaScript programming

Publications

    also see more details
  • Oct 2026
    Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic
    Egor Namakonov, Justus Fasse, Bart Jacobs, Lars Birkedal, Amin Timany
  • Feb 2026
    Verifying wait-freedom of higher-order programs [preprint]
    Egor Namakonov, Lars Birkedal, Amin Timany
  • Oct 2021
    Making weak memory models fair
    Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis
  • Dec 2019
    Compilation of OCaml memory model into Power
    Egor Namakonov, Anton Podkopaev

Skills

Programming languages
OCaml
Python
Rust
also: Haskell, C, Java, Kotlin, Elisp, Groovy...
Formal verification tools
Rocq proof assistant
Iris separation logic
Automation tools
Vagrant
Docker
Travis CI
Jenkins
Theory
Formal logic
Dependent types

Languages

Russian
Native speaker
English
Fluent
Danish
Intermediate
German
Beginner

Professional interests

Formal verification
Concurrency
Weak memory
Liveness

Projects

  • Mar 2019 - Aug 2022
    Intermediate Memory Model
    A declarative memory model bridging the gap between the models of languages and processors
  • Sep 2022 - present
    Trillium
    Concurrent separation logic for proving refinement between programs and abstract models

Misc