System Description: GAPT 2.0. - Gabriel Ebner; Stefan Hetzl; Giselle Reis; Martin Riener; Simon Wolfsteiner; Sebastian Zivota (IJCAR, 2016)

A metaprogramming framework for formal verification. - Gabriel Ebner; Sebastian Ullrich 002; Jared Roesch; Jeremy Avigad; Leonardo de Moura 001 (Proc. ACM Program. Lang., 2017)

Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars. - Sebastian Eberhard; Gabriel Ebner; Stefan Hetzl (ACM Trans. Comput. Log., 2017)

Efficient Translation of Sequent Calculus Proofs Into Natural Deduction Proofs. - Gabriel Ebner; Matthias Schlaipfer (PAAR@FLoC, 2018)

Complexity of Decision Problems on Totally Rigid Acyclic Tree Grammars. - Sebastian Eberhard; Gabriel Ebner; Stefan Hetzl (DLT, 2018)

Fast Cut-Elimination using Proof Terms: An Empirical Study. - Gabriel Ebner (CL&C, 2018)

Herbrand Constructivization for Automated Intuitionistic Theorem Proving. - Gabriel Ebner (TABLEAUX, 2019)

On the Generation of Quantified Lemmas. - Gabriel Ebner; Stefan Hetzl; Alexander Leitsch; Giselle Reis; Daniel Weller 001 (J. Autom. Reason., 2019)

Maintaining a Library of Formal Mathematics. - Floris van Doorn; Gabriel Ebner; Robert Y. Lewis (CICM, 2020)

A Unifying Splitting Framework. - Gabriel Ebner; Jasmin Blanchette; Sophie Tourret (CADE, 2021)

HyperTree Proof Search for Neural Theorem Proving. - Guillaume Lample; Timothée Lacroix; Marie-Anne Lachaux; Aurélien Rodriguez; Amaury Hayat; Thibaut Lavril; Gabriel Ebner; Xavier Martinet (NeurIPS, 2022)

An Extensible User Interface for Lean 4. - Wojciech Nawrocki; Edward W. Ayers; Gabriel Ebner (ITP, 2023)

Symbolic Automata: ω-Regularity Modulo Theories. - Margus Veanes; Thomas Ball 001; Gabriel Ebner; Olli Saarikivi (CoRR, 2023)

Unifying Splitting. - Gabriel Ebner; Jasmin Blanchette; Sophie Tourret (J. Autom. Reason., 2023)

Lean Formalization of Extended Regular Expression Matching with Lookarounds. - Ekaterina Zhuchko; Margus Veanes; Gabriel Ebner (CPP, 2024)

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming. - Saikat Chakraborty; Gabriel Ebner; Siddharth Bhat; Sarah Fakhoury; Sakina Fatima; Shuvendu K. Lahiri; Nikhil Swamy (ICSE, 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 (Proc. ACM Program. Lang., 2025)

Symbolic Automata: Omega-Regularity Modulo Theories. - Margus Veanes; Thomas Ball 001; Gabriel Ebner; Ekaterina Zhuchko (Proc. ACM Program. Lang., 2025)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE. - Tahina Ramananandro; Gabriel Ebner; Guido Martínez; Nikhil Swamy (CoRR, 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 001; Sarah Fakhoury (CoRR, 2025)