Papers

On the generation of quantified lemmas
(with S. Hetzl, A. Leitsch, G. Reis, and D. Weller)
Journal of Automated Reasoning (2018)
pdf, Springer

Algorithmic compression of finite tree languages by rigid acyclic grammars
(with S. Eberhard and S. Hetzl)
ACM Transactions on Computational Logic 18(4) (2017)
pdf, ACM

A metaprogramming framework for formal verification
(with S. Ullrich, J. Roesch, J. Avigad, and L. de Moura)
Proceedings of the ACM on Programming Languages 1(ICFP) (2017)
pdf, ACM

System description: GAPT 2.0
(with S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner, and S. Zivota)
IJCAR 2016, N. Olivetti and A. Tiwari (eds.), Springer LNCS 9706
pdf, slides, Springer

Talks

Extracting expansion trees from resolution proofs with splitting and definitions
Theory & Logic seminar at TU Wien, January 17, 2018, slides.

The Lean Theorem Prover
Alpine Verification Meeting 2017, September 18, 2017, slides, materials.

Complexity of decision problems on TRATGs
Herbrand’s Theorem Revisited (workshop), May 5, 2017, slides.

The Lean Theorem Prover
(with L. de Moura, J. Roesch, and S. Ullrich)
POPL 2017, January 16, 2017, slides, materials.

Minimal grammars via MaxSAT
Theory & Logic seminar at TU Wien, April 13, 2016, slides.

Finding loop invariants using tree grammars
Theory & Logic seminar at TU Wien, January 28, 2015, slides.

Preprints

Complexity of decision problems on totally rigid acyclic tree grammars (2018)
(with S. Eberhard and S. Hetzl)
pdf

Efficient translation of sequent calculus proofs into natural deduction proofs (2018)
(with M. Schlaipfer)
pdf

Fast cut-elimination using proof terms: an empirical study (2018)
pdf

Extracting expansion trees from resolution proofs with splitting and definitions (2018)
pdf

Tree grammars for induction on inductive data types modulo equational theories (2018)
(with S. Hetzl)
pdf