RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
Ashkan Vedadi Gargary, Guido Martínez, Sebastian Burckhardt, Gabriel Ebner, Abhinav Jangda, Madan Musuvathi, Tyler Sorensen
October 2026
arXiv | October 2026
Gabriel Ebner
Research Software Engineer
出版物
-
-
-
-
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
Computer and Communications Security | October 2025
-
What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
Rijul Jain, Shraddha Barke, Gabriel Ebner, Md Rakib Hossain Misu, Shan Lu, Sarah Fakhoury
August 2025
-
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
Programming Language Design and Implementation | June 2025
-
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
International Conference on Software Engineering | April 2025
-
-
-
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
CPP | January 2024
-
-
-
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
-
-
-
RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
Ashkan Vedadi Gargary, Guido Martínez, Sebastian Burckhardt, Gabriel Ebner, Abhinav Jangda, Madan Musuvathi, Tyler Sorensen
October 2026
arXiv | October 2026
-
-
-
RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
Ashkan Vedadi Gargary, Guido Martínez, Sebastian Burckhardt, Gabriel Ebner, Abhinav Jangda, Madan Musuvathi, Tyler Sorensen
October 2026
arXiv | October 2026
-
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
Computer and Communications Security | October 2025
-
What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
Rijul Jain, Shraddha Barke, Gabriel Ebner, Md Rakib Hossain Misu, Shan Lu, Sarah Fakhoury
August 2025
-
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
Programming Language Design and Implementation | June 2025
-
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
International Conference on Software Engineering | April 2025
-
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
CPP | January 2024
-
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
-
-
-
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
Computer and Communications Security | October 2025
-
-
-
What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
Rijul Jain, Shraddha Barke, Gabriel Ebner, Md Rakib Hossain Misu, Shan Lu, Sarah Fakhoury
August 2025
-
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
-
-
-
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
-
-
-
RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
Ashkan Vedadi Gargary, Guido Martínez, Sebastian Burckhardt, Gabriel Ebner, Abhinav Jangda, Madan Musuvathi, Tyler Sorensen
October 2026
arXiv | October 2026
-
-
-
Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
Computer and Communications Security | October 2025
-
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
Programming Language Design and Implementation | June 2025
-
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
International Conference on Software Engineering | April 2025
-
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
CPP | January 2024
-
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
ICFP 2017 | August 2017
-
-
-
What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
Rijul Jain, Shraddha Barke, Gabriel Ebner, Md Rakib Hossain Misu, Shan Lu, Sarah Fakhoury
August 2025
-