cv

Basics

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

Professional interests

Concurrency
Systems programming
Formal verification
Weak memory
Liveness

Skills

Programming languages
Rust (+ tokio)
OCaml
Python
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

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

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

Projects

  • Jul 2026 - Present
    tubu
    Personal project for practicing async Rust w/ tokio and some aspects of systems programming
  • 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

Teaching

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
  • Jun 2026
    Verifying wait-freedom for concurrent higher-order programs
    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

Languages

Russian
Native speaker
English
Fluent
Danish
Intermediate
German
Beginner

Misc