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 trustworthy formal verification based on interactive proof assistants (especially Coq), with applications to trustworthy compilation of floating points, trustworthy model-checking, and trustworthy automated bug finding. More recently, I have been working on using proof assistants to verify hyperproperties of programs in the context of the ERC advanced grant HYPER.

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!

Teaching

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

Service

  • (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

Awards

  • 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.