Egor Namakonov

PhD student working on formal verification of concurrent programs
e.namakonov@cs.au.dk, https://fresheed.github.io
Aarhus, Denmark

Professional interests

Formal verification, Concurrency, Weak memory, Liveness

Publications

October 2026: Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic
February 2026: Verifying wait-freedom of higher-order programs [preprint]
October 2021: Making weak memory models fair
December 2019: Compilation of OCaml memory model into Power

Education

September 2022 – present : PhD in Computer Science, Aarhus University
September 2018 – July 2020 : Master in Computer Science, St Petersburg University
September 2013 – July 2017 : Bachelor in Software Engineering, Peter the Great St. Petersburg Polytechnic University

Industry experience

July 2019 – August 2022 : JetBrains Research (St. Petersburg, Russia) — Intern and junior researcher

Weak memory research, teaching

November 2015 – July 2018 : OpenWay Group (St. Petersburg, Russia) — Intern and DevOps engineer

Continuous Integration, internal Python development, VM administration

Volunteering

June 2022 – November 2022 : Helping to Leave (Remote) — Software engineer

DSL-based chatbots development, JavaScript programming

June 2022 – May 2024 : OVD-Info (Remote) — Software engineer

Python chatbots development, CI

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