Cezar-Constantin Andrici

Academic Activity

Publications

Submitted to ESOP’27
A Taxonomy of Predicate Transformer Monads for Specifying Monadic ProgramsAbigail Pribisova, Yao Li, Cezar-Constantin Andrici, Cătălin Hrițcu, Kenji Maillard, and Exequiel Rivas.
ICFP 2026
Misquoted No More: Securely Extracting F* programs with IOCezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas, and Théo Winterhalter. DOISlidesVideoArtifactThe artifact received the Functional and Reusable badges.
ICFP 2025
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*Cezar-Constantin Andrici, Danel Ahman, Cătălin Hrițcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, and Théo Winterhalter. DOISlidesVideoArtifactThe artifact received the Functional and Reusable badges.
POPL 2024
Securing Verified IO Programs Against Unverified Code in F*Cezar-Constantin Andrici, Ștefan Ciobâcă, Cătălin Hrițcu, Guido Martínez, Exequiel Rivas, Éric Tanter and Théo Winterhalter. DOIVideoPoP Up VideoArtifactThe artifact received the Functional and Reusable badges.
Mathematics 2022
A Verified Implementation of the DPLL Algorithm in DafnyCezar-Constantin Andrici and Ștefan Ciobâcă. Artifact
HOPE 2022
Verifying non-terminating programs with IO in F* (Extended Abstract)Cezar-Constantin Andrici, Théo Winterhalter, Cătălin Hrițcu and Exequiel Rivas. SlidesVideoArtifact
TYPES 2022
Partial Dijkstra Monads for All (Extended Abstract)Théo Winterhalter, Cezar-Constantin Andrici, Cătălin Hrițcu, Kenji Maillard, Guido Martínez and Exequiel Rivas. Artifact
FROM 2019
Verifying the DPLL Algorithm in DafnyCezar-Constantin Andrici and Ștefan Ciobâcă.

Talks

For the conference presentations of my papers, see the Slides and Video links under Publications.

Aarhus 2026
Secure extraction of verified effectful F* programs to MLAt Aarhus University, April 13, 2026. Slides
ICFP SRC 2020
Gradual Enforcement of IO Trace Properties at Student Research CompetitionAt the 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2020. Video🏆 First place winner of ICFP SRC 2020, graduate section.
UAIC 2020
Verification of IO programs in F*At the Faculty of Computer Science, UAIC, January 2020.

Teaching

2024–2025
Proofs are Programs — Teaching Assistant, RUB, Bochum (Fall)
2023–2024
Functional Programming — Teaching Assistant, RUB, Bochum (Summer)
2020–2021
Logics in Computer Science — Teaching Assistant, UAIC, Iași (Fall)

Academic Service

Sub-reviewer
CPP’26, ICFP’25, POPL’24, SP’21
Artifact Evaluation
Committee member at POPL’26, POPL’23
Student Volunteer
POPL’24, POPL’23, ICFP’22, PLDI’20, POPL’20, ETAPS’19, FROM’18