Splitting Proofs for Interpolation. - Bernhard Gleiss; Laura Kovács; Martin Suda 001 (CADE, 2017)

Loop Analysis by Quantification over Iterations. - Bernhard Gleiss; Laura Kovács; Simon Robillard (LPAR, 2018)

Local Soundness for QBF Calculi. - Martin Suda 001; Bernhard Gleiss (SAT, 2018)

Verifying Relational Properties using Trace Logic. - Gilles Barthe; Renate Eilers; Pamina Georgiou; Bernhard Gleiss; Laura Kovács; Matteo Maffei (FMCAD, 2019)

Interactive Visualization of Saturation Attempts in Vampire. - Bernhard Gleiss; Laura Kovács; Lena Schnedlitz (IFM, 2019)

Layered Clause Selection for Theory Reasoning - (Short Paper). - Bernhard Gleiss; Martin Suda 001 (IJCAR (1), 2020)

Layered Clause Selection for Saturation-Based Theorem Proving. - Bernhard Gleiss; Martin Suda 001 (PAAR+SC²@IJCAR, 2020)

Subsumption Demodulation in First-Order Theorem Proving. - Bernhard Gleiss; Laura Kovács; Jakob Rath (IJCAR (1), 2020)

Trace Logic for Inductive Loop Reasoning. - Pamina Georgiou; Bernhard Gleiss; Laura Kovács (FMCAD, 2020)

Layered Clause Selection for Theory Reasoning. - Bernhard Gleiss; Martin Suda 001 (CoRR, 2020)

The Rapid Software Verification Framework. - Pamina Georgiou; Bernhard Gleiss; Ahmed Bhayat; Michael Rawson 001; Laura Kovács; Giles Reger (FMCAD, 2022)