I’m a Ph.D. candidate at MPI-SP, Bochum, Germany working with Cătălin Hriţcu. My Ph.D. project is about secure interoperability between verified F* programs and unverified ML code. I earned my Bachelor’s and Master’s degrees in Computer Science from Alexandru Ioan Cuza University of Iași, Romania. I also hold a Master’s degree in Regional Development from the same university.
Research interests
Verification of effectful code. In a pure dependently-typed language, like Rocq or F*, one can write pure terminating computations and verify them. If one wants to write effectful computations (e.g., with state, non-termination, input/output (IO), etc.), then one has to give a representation to those computations. One common way is to do a shallow embedding, by embedding the effect in the language using a monad. F* has this idea at its core and uses a construction called the Dijkstra monad. Such constructions were used successfully to verify big developments and realistic projects. My work in this space was involved into finding the pre-conditional effect (specific to F*), and building Dijkstra monads for terminating/non-terminating IO and Monotonic State. These results are interesting because the effects F* supports out of the box do not have a monadic representation (are axiomatized), and if one finds a representation for each of them, the TCB of F* would be minimized. Right now, I am interested in finding a monadic representation for the effects Div, Ghost, Monotonic State with higher-order stores, and Concurrency with IO.
Secure Compilation of F*. The language F* was used successfully in the verification of some big projects, some of them milestones in the verification community. One convenient feature of F* is primitive extraction to OCaml of effectful computations, meaning that the monadic representation of the computation is erased during extraction and the monad’s operations are replaced with the corresponding OCaml operations. This extraction, however, it is part of the TCB of F* so it is not verified to be correct. Moreover, if the verified extracted code gets linked to unverified code, then there is a chance of a bug, or an attack, so it may be even insecure (the logical invariants proved about the verified code are broken by the unverified code). To bring some trust to this, my work proposes SCIO* and SecRef*, two secure compilation frameworks for verified IO programs, and respectively stateful programs, that can be safely linked with unverified code. The long-term goal of the project is to have secure interoperability between F* and OCaml.
Publications, drafts and extended abstracts
- 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. - 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.
In 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2024.
Artifact - The artifact received the Functional and Reusable badges. - A Verified Implementation of the DPLL Algorithm in Dafny.
Cezar-Constantin Andrici and Ștefan Ciobâcă. In Mathematics, 10(13), 2264, June 2022.
Artifact - Verifying non-terminating programs with IO in F* (Extended Abstract).
Cezar-Constantin Andrici, Théo Winterhalter, Cătălin Hrițcu and Exequiel Rivas.
At the 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE), September 2022.
Artifact - 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.
At the 28th International Conference on Types for Proofs and Programs (TYPES), June 2022.
Artifact - Verifying the DPLL Algorithm in Dafny.
Cezar-Constantin Andrici and Ștefan Ciobâcă.
In Proceedings Third Symposium on Working Formal Methods, EPTCS 303, pp. 3-15, 2019.
Talks
- Securing Verified IO Programs Against Unverified Code in F*.
At the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2024 (Video),
and an extended version at the F* PoP Up Seminar, July 2023 - (video). - Verifying non-terminating programs with IO in F* (Extended Abstract).
At the 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE), September 2022.
Slides. Video. - Gradual Enforcement of IO Trace Properties at Student Research Competition,
At the 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2020.
Video - Verification of IO programs in F* at Faculty of Computer Science, UAIC, January 2020.
Teaching Assistant
- Proofs are Programs, RUB, Bochum, WS 2024-2025
- Functional Programming, RUB, Bochum, SS 2023-2024
- Logics in Computer Science, UAIC, Iași, WS 2020-2021
Scientific Service
- Sub-reviewer at ICFP’25, POPL’24, SP’21
- Member in Artifact Evaluation Committee at POPL’23
- Student Volunteer at POPL’24, POPL’23, ICFP’22, PLDI’20, POPL’20, ETAPS’19, FROM’18