Generalized Reactivity(1) Synthesis without a Monolithic Strategy. - Matthias Schlaipfer; Georg Hofferek; Roderick Bloem (Haifa Verification Conference, 2011)

Reduction of Resolution Refutations and Interpolants via Subsumption. - Roderick Bloem; Sharad Malik; Matthias Schlaipfer; Georg Weissenbacher (Haifa Verification Conference, 2014)

Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs. - Matthias Schlaipfer; Georg Weissenbacher (J. Autom. Reason., 2016)

Optimizing Big-Data Queries Using Program Synthesis. - Matthias Schlaipfer; Kaushik Rajan; Akash Lal; Malavika Samak (SOSP, 2017)

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

Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. - Matthias Schlaipfer; Friedrich Slivovsky; Georg Weissenbacher; Florian Zuleger (SAT, 2020)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)