Dr. Anton Podkopaev photo

Prof. Dr. Anton Podkopaev

Email Address
apodkopaev@constructor.university
Research Interests
  • Combination of formal methods and generative AI
  • Programming Languages
  • Program verification
  • Interactive theorem proving
  • Weak memory models, concurrency
University Education
  • Saint Petersburg State University
    PhD, Computer Science
    2014 - 2018
  • Saint Petersburg State University
    Specialist, Mathematics and Computer Science
    2009 - 2014
Research and Teaching Positions
Jan 2024 - PresentJetBrains - Head of Programming Languages and Program Analysis (PLAN) lab
Mar 2023 - PresentConstructor University - Adjunct Professor
Jun 2022 - Jan 2024JetBrains - Head of Programming Languages and Tools (PLT) Lab
Apr 2018 - Jun 2022JetBrains - Senior Researcher
Feb 2018 - May 2022Computer Science Center - Lecturer
Nov 2018 - Jun 2022HSE University - Associate Professor
Jun 2019 - Oct 2020MPI SWS - Postdoctoral Researcher
Oct 2013 - Apr 2018JetBrains - Researcher
Sep 2015 - Aug 2018St. Petersburg Academic University of the Russian Academy of Sciences - Lecturer
May 2016 - Aug 2016Max Planck Institute for Software Systems - Research Intern
Jun 2015 - Aug 2015IMDEA Software Institute - Research Intern
Nov 2012 - Sep 2013JetBrains - Research Intern
Selected Publications
  • Relaxed Memory Concurrency Re-executed
    Authors: E. Moiseenko, M. Meluzzi, I. Meleshchenko, I. Kabashnyi, A. Podkopaev, S. Chakraborty
    Conference: Symposium on Principles of Programming Languages, POPL 2025
    Links: Paper, DOI
    Award: Distinguished Paper Award
  • LitmusKt: Concurrency Stress Testing for Kotlin
    Authors: D. Lochmelis, E. Moiseenko, Y. Golubev, A. Podkopaev
    Conference: International Conference on the Foundations of Software Engineering, FSE 2025
    Links: arXiv
  • CoqPilot, a Plugin for LLM-based Generation of Proofs
    Authors: A. Kozyrev, G. Solovev, N. Khramov, A. Podkopaev
    Conference: International Conference on Automated Software Engineering, ASE 2024
    Links: Draft, arXiv, Video (5 min), Video (10 min), GitHub
  • Can LLMs Enable Verification in Mainstream Programming?
    Authors: A. Shefer, I. Engel, S. Alekseev, D. Berezun, E. Verbitskaia, A. Podkopaev
    Links: arXiv
  • The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
    Authors: A. Jeffrey, J. Riely, M. Batty, S. Cooksey, I. Kaysin, A. Podkopaev
    Conference: Symposium on Principles of Programming Languages, POPL 2022
    Links: Paper, Full paper, Project, Artifact @Zenodo, GitHub

Explore more