Papers & Talks
Publications, drafts and extended abstracts
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. 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 |