Gabriel Ebner

Research Software Engineer

Publications

View by:

- Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
  
  Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
  
  2025 Computer and Communications Security | October 2025
  
  Publication Preprint Author's Version Project
- 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
  
  Preprint
- 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
  
  2025 Programming Language Design and Implementation | June 2025
  
  Accepted for publication, to appear
  
  Author's Version Project
- Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
  
  Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
  
  2025 International Conference on Software Engineering | April 2025
  
  Preprint Access Access Project
- Lean Formalization of Extended Regular Expression Matching with Lookarounds
  
  Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
  
  CPP | January 2024
  
  Author's Version DOI Project
- A metaprogramming framework for formal verification
  
  Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
  
  ICFP 2017 | August 2017
  
  DOI PDF Github Project

- Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
  
  Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
  
  2025 Computer and Communications Security | October 2025
  
  Publication Preprint Author's Version Project
- 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
  
  Preprint
- 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
  
  2025 Programming Language Design and Implementation | June 2025
  
  Accepted for publication, to appear
  
  Author's Version Project
- Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
  
  Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
  
  2025 International Conference on Software Engineering | April 2025
  
  Preprint Access Access Project
- Lean Formalization of Extended Regular Expression Matching with Lookarounds
  
  Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
  
  CPP | January 2024
  
  Author's Version DOI Project
- A metaprogramming framework for formal verification
  
  Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
  
  ICFP 2017 | August 2017
  
  DOI PDF Github Project
- Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
  
  Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
  
  2025 Computer and Communications Security | October 2025
  
  Publication Preprint Author's Version Project
- 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
  
  Preprint
- A metaprogramming framework for formal verification
  
  Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
  
  ICFP 2017 | August 2017
  
  DOI PDF Github Project
- A metaprogramming framework for formal verification
  
  Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
  
  ICFP 2017 | August 2017
  
  DOI PDF Github Project

- Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
  
  Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
  
  2025 Computer and Communications Security | October 2025
  
  Publication Preprint Author's Version Project
- 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
  
  2025 Programming Language Design and Implementation | June 2025
  
  Accepted for publication, to appear
  
  Author's Version Project
- Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
  
  Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
  
  2025 International Conference on Software Engineering | April 2025
  
  Preprint Access Access Project
- Lean Formalization of Extended Regular Expression Matching with Lookarounds
  
  Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
  
  CPP | January 2024
  
  Author's Version DOI Project
- A metaprogramming framework for formal verification
  
  Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
  
  ICFP 2017 | August 2017
  
  DOI PDF Github Project
- 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
  
  Preprint

Gabriel Ebner

Publications

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

Lean Formalization of Extended Regular Expression Matching with Lookarounds

A metaprogramming framework for formal verification

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

Lean Formalization of Extended Regular Expression Matching with Lookarounds

A metaprogramming framework for formal verification

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus

A metaprogramming framework for formal verification

A metaprogramming framework for formal verification

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

Lean Formalization of Extended Regular Expression Matching with Lookarounds

A metaprogramming framework for formal verification

What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus

Contact Gabriel Ebner

Microsoft Research Lab – Redmond