About Me
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!
- Email : arthur.correnson@cispa.de
- GitHub : acorrenson
- LinkedIn : Arthur Correnson
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
Teaching
I truly enjoy teaching! I have been involved in the organization of many lectures at Saarland University.- (2023-2024) Teaching Assistant for the lecture Verification
- (2023) Teaching Assistant for the seminar Hyper Properties
- (2022-2023) Teaching Assistant for the lecture Automata, Games and Verification
- (2021-2022) Tutor for the lecture Automated Reasoning
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.