3 citations · 3 across the 3 of their papers we have counts for
4 papers
RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
Ashkan Vedadi Gargary, Guido Martínez, Sebastian Burckhardt +4
AI systems can now write and optimize production GPU kernels, but validating them remains an important challenge. Evaluating the kernel on a few random inputs and checking that its…
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…
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…
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat +4
Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite th…