I’m a third-year Ph.D. candidate at the Max Planck Institute for Security and Privacy (MPI-SP) in Bochum, Germany working with Cătălin Hriţcu. My research interests center around using formal methods to build correct and secure technology that protects privacy. I implemented and formally verified a SAT solver in the Dafny programming language. I devised in the F★ programming language a secure compiler for IO programs that is formally verified to satisfy one of the strongest criteria of secure compilation. You can find my updated Resume / CV here and contact me at cezar.andrici@mpi-sp.org.
News
My most recent paper was accepted at POPL 2024!
Recent Publications and Drafts
- 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. Accepted at POPL 2024. The artifact received the Functional and Reusable badges.
- Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny. Cezar-Constantin Andrici and Ștefan Ciobâcă. In Mathematics 2022, 10(13), 2264.
- 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 2022). Slides. Video.
- 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 2022).