Cezar-Constantin Andrici

PhD working on ways to practically verify code and to securely compile it.

Publications, drafts and extended abstracts

2025

Draft 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.
PrePrint.

2024

POPL’24 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. The artifact received the Functional and Reusable badges.
PrePrint. Video. Artifact

2022

  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.
Artifact
HOPE’22 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.
Slides. Video. Artifact
TYPES’22 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.
Slides. Artifact