5 citations · 9 across the 5 of their papers we have counts for
5 papers
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman +3
Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded program…
SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*
Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu +4
We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style…
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu +4
We introduce SCIO*, a formally secure compilation framework for statically verified partial programs performing input-output (IO). The source language is an F* subset in which a ve…
Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny
Cezar-Constantin Andrici, Ştefan Ciobâcă
We build a SAT solver implementing the DPLL algorithm in the verification-enabled programming language Dafny. The resulting solver is fully verified (soundness, completeness and te…
Verifying the DPLL Algorithm in Dafny
Cezar-Constantin Andrici, Ştefan Ciobâcă
Modern high-performance SAT solvers quickly solve large satisfiability instances that occur in practice. If the instance is satisfiable, then the SAT solver can provide a witness w…