| 2026 | IJCAR | A Two-Watched Literal Scheme for First-Order Logic. | Yasmine Briefs, Martin Bromberger, Tobias Gehl, Lorenz Leutgeb, Simon Schwarz, Christoph Weidenbach |
| 2025 | CADE | A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution. | Martin Bromberger, Martin Desharnais, Christoph Weidenbach |
| 2025 | CADE | Computing Ground Congruence Classes. | Hendrik Leidinger, Christoph Weidenbach |
| 2024 | IJCAR | First-Order Automatic Literal Model Generation. | Martin Bromberger, Florent Krasnopol, Sibylle Mhle, Christoph Weidenbach |
| 2024 | LPAR | Automatic Bit- and Memory-Precise Verification of eBPF Code. | Martin Bromberger, Simon Schwarz, Christoph Weidenbach |
| 2023 | CADE | An Isabelle/HOL Formalization of the SCL(FOL) Calculus. | Martin Bromberger, Martin Desharnais, Christoph Weidenbach |
| 2023 | CADE | SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. | Martin Bromberger, Chaahat Jain, Christoph Weidenbach |
| 2023 | LPAR | Exploring Partial Models with SCL. | Martin Bromberger, Simon Schwarz, Christoph Weidenbach |
| 2022 | CADE | An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. | Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach |
| 2022 | CADE | Connection-Minimal Abduction in | Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach |
| 2022 | CADE | Semantic Relevance. | Fajar Haifani, Christoph Weidenbach |
| 2022 | CADE | SCL(EQ): SCL for First-Order Logic with Equality. | Hendrik Leidinger, Christoph Weidenbach |
| 2022 | TACAS | A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. | Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry Gonzlez, Markus Krtzsch, Maximilian Marx, Harish K. Murali, Christoph Weidenbach |
| 2021 | CADE | Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. | Fajar Haifani, Sophie Tourret, Christoph Weidenbach |
| 2021 | VMCAI | Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. | Martin Bromberger, Alberto Fiori, Christoph Weidenbach |
| 2020 | ISoLA | Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification. | Rasha Faqeh, Christof Fetzer, Holger Hermanns, Jrg Hoffmann, Michaela Klauck, Maximilian A. Khl, Marcel Steinmetz, Christoph Weidenbach |
| 2020 | LPAR | A Verified SAT Solver Framework including Optimization and Partial Valuations. | Mathias Fleury, Christoph Weidenbach |
| 2019 | CADE | SPASS-SATT - A CDCL(LA) Solver. | Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach |
| 2019 | CADE | SCL Clause Learning from Simple Models. | Alberto Fiori, Christoph Weidenbach |
| 2017 | CADE | On the Combination of the Bernays-Schnfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. | Matthias Horbach, Marco Voigt, Christoph Weidenbach |
| 2017 | CADE | Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. | Andreas Teucke, Christoph Weidenbach |
| 2017 | CADE | Do Portfolio Solvers Harm? | Christoph Weidenbach |
| 2017 | IJCAI | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. | Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach |
| 2016 | CADE | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. | Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach |
| 2016 | CADE | Fast Cube Tests for LIA Constraint Solving. | Martin Bromberger, Christoph Weidenbach |
| 2016 | CADE | Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. | Martin Bromberger, Christoph Weidenbach |
| 2016 | CADE | A Dynamic Logic for Configuration. | Ching Hoo Tang, Christoph Weidenbach |
| 2016 | CADE | Ordered Resolution with Straight Dismatching Constraints. | Andreas Teucke, Christoph Weidenbach |
| 2016 | ISoLA | Compliance, Functional Safety and Fault Detection by Formal Methods. | Christof Fetzer, Christoph Weidenbach, Patrick Wischnewski |
| 2016 | LICS | Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. | Thomas Sturm, Marco Voigt, Christoph Weidenbach |
| 2015 | CADE | Linear Integer Arithmetic Revisited. | Martin Bromberger, Thomas Sturm, Christoph Weidenbach |
| 2013 | CADE | Computing Tiny Clause Normal Forms. | Noran Azmy, Christoph Weidenbach |
| 2013 | LPAR | BDI: A New Decidable First-order Clause Class. | Manuel Lamotte-Schubert, Christoph Weidenbach |
| 2012 | CADE | Combination of Disjoint Theories: Beyond Decidability. | Pascal Fontaine, Stephan Merz, Christoph Weidenbach |
| 2012 | CADE | A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. | Martin Suda, Christoph Weidenbach |
| 2012 | CADE | Satisfiability Checking and Query Answering for Large Ontologies. | Christoph Weidenbach, Patrick Wischnewski |
| 2012 | ITP | More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. | Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach |
| 2012 | LPAR | Automatic Generation of Invariants for Circular Derivations in SUP(LA). | Arnaud Fietzke, Evgeny Kruglov, Christoph Weidenbach |
| 2012 | LPAR | Labelled Superposition for PLTL. | Martin Suda, Christoph Weidenbach |
| 2011 | FORTE | Towards Verification of the Pastry Protocol Using TLA | Tianxiang Lu, Stephan Merz, Christoph Weidenbach |
| 2010 | CADE | On the Saturation of YAGO. | Martin Suda, Christoph Weidenbach, Patrick Wischnewski |
| 2010 | LPAR | Superposition-Based Analysis of First-Order Probabilistic Timed Automata. | Arnaud Fietzke, Holger Hermanns, Christoph Weidenbach |
| 2009 | CADE | Decidability Results for Saturation-Based Model Building. | Matthias Horbach, Christoph Weidenbach |
| 2009 | CADE | SPASS Version 3.5. | Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski |
| 2009 | CSL | Deciding the Inductive Validity of FOR ALL THERE EXISTS | Matthias Horbach, Christoph Weidenbach |
| 2008 | CADE | Labelled Splitting. | Arnaud Fietzke, Christoph Weidenbach |
| 2008 | CADE | Contextual Rewriting in SPASS. | Christoph Weidenbach, Patrick Wischnewski |
| 2008 | CSL | Superposition for Fixed Domains. | Matthias Horbach, Christoph Weidenbach |
| 2007 | CADE | Labelled Clauses. | Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv |
| 2007 | CADE | System Description: SpassVersion 3.0. | Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic |
| 2002 | CADE | S PASS Version 2.0. | Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobalt, Dalibor Topic |
| 2001 | LPAR | First-Order Atom Definitions Extended. | Bijan Afshordel, Thomas Hillenbrand, Christoph Weidenbach |
| 1999 | CADE | Towards an Automatic Analysis of Security Protocols in First-Order Logic. | Christoph Weidenbach |
| 1999 | CADE | System Description: Spass Version 1.0.0. | Christoph Weidenbach |
| 1998 | CADE | On Generating Small Clause Normal Forms. | Andreas Nonnengart, Georg Rock, Christoph Weidenbach |
| 1997 | CADE | Soft Typing for Ordered Resolution. | Harald Ganzinger, Christoph Meyer, Christoph Weidenbach |
| 1996 | CADE | Unification in Pseudo-Linear Sort Theories is Decidable. | Christoph Weidenbach |
| 1996 | CADE | SPASS & FLOTTER Version 0.42. | Christoph Weidenbach, Bernd Gaede, Georg Rock |
| 1993 | IJCAI | Extending the Resolution Method with Sorts. | Christoph Weidenbach |
| 1992 | KI | A New Sorted Logic. | Christoph Weidenbach |
| 1990 | ECAI | A Resolution Calculus with Dynamic Sort Structures and Partial Functions. | Christoph Weidenbach, Hans Jrgen Ohlbach |