Arthur Correnson

About Me

A picture of Arthur Correnson

I am a PhD candidate at CISPA under the supervision of Bernd Finkbeiner. My research focuses on formal verification using interactive proof assistants (especially Coq, which is my favorite proof assistant). In particular, I am interested in proving the correctness of critical tools such as compilers, static analyzers, automated provers etc. More generally, I am curious about pretty much everything related to programming languages and verification (semantics, logic, category theory, ...).

Feel free to send me an email for any question related to my research! I'm also very happy to discuss any research oriented project, especially if it involves proving stuff!

Exciting news!

  • (2023) I will be at ESEC/FSE in San Fransisco to present my work on the formal verification of automated bug finders
  • (2023) I am advising the bachelor thesis of Iona Kuhn on the Coq formalization of algorithms for omega regular expressions
  • (2022) I was honored to win ICFP Student Research Competition in the graduate category


I truly enjoy teaching! I have been involved in the organization of many lectures at Saarland University.


  • (2024) POPL Student Volunteer
  • (2023) TACAS Subreviewer
  • (2023) DATE Subreviewer
  • (2023) ATVA Subreviewer
  • (2023) ICFP Artifact Evaluation Committee
  • (2022) ICFP Student Volunteer

Experiences in academia and in industry

  • (2022-2023) Part time employee at AbsInt GmbH.
    Proof engineering for the CompCert compiler
  • (Summer 2021) Intern at CEA, Software Safety & Security Lab.
    Formal verification of constraint propagators for floating point arithmetic
  • (Summer 2019) Intern at INRIA in the team DYLISS.
    Implementation of algorithms for the alignment of biological sequences


  • Best artifact awards at ESEC\FSE 2023 for the paper Engineering a Formally Verified Automated Bug Finder
  • First prize of ICFP-SRC 2022 for my work Formal Verification of a Lazy Abstraction Model Checker

Other Activities

Aside from research and studies, I dedicate my free-time to the popularization of theoretical computer science. I co-founded the student organization CodeAnon that organises conferences, tutorials and workshops for undergrad students at University Toulouse III.