2 papers
cs.SE2025
What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
Rijul Jain, Shraddha Barke, Gabriel Ebner +3
Proof-oriented programming languages (POPLs) empower developers to write code alongside formal correctness proofs, providing formal guarantees that the code adheres to specified re…
cs.CR2025
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido MartÃnez +1
Incorrect handling of security-critical data formats, particularly in low-level languages, are the root cause of many security vulnerabilities. Provably correct parsing and seriali…