Verifying the DPLL Algorithm in Dafny. - Cezar-Constantin Andrici; Stefan Ciobaca (FROM, 2019)

Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny. - Cezar-Constantin Andrici; Stefan Ciobaca (CoRR, 2020)

Securely Compiling Verified F* Programs With IO. - Cezar-Constantin Andrici; Catalin Hritcu; Guido Martínez; Exequiel Rivas; Théo Winterhalter (CoRR, 2023)

Securing Verified IO Programs Against Unverified Code in F. - Cezar-Constantin Andrici; Stefan Ciobaca; Catalin Hritcu; Guido Martínez; Exequiel Rivas; Éric Tanter; Théo Winterhalter (Proc. ACM Program. Lang., 2024)

SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F. - Cezar-Constantin Andrici; Danel Ahman; Catalin Hritcu; Ruxandra Icleanu; Guido Martínez; Exequiel Rivas; Théo Winterhalter (CoRR, 2025)