Christoph Weidenbach

132 papers A* 4A 34B 10C 1Journal 43Unranked 35

Year	Rank	Type	Title / Venue / Authors
2026	—	`ed.`	Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings FroCoS René Thiemann, Christoph Weidenbach
2025	A	`conf`	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution. CADE Martin Bromberger, Martin Desharnais, Christoph Weidenbach
2025	A	`conf`	Computing Ground Congruence Classes. CADE Hendrik Leidinger, Christoph Weidenbach
2024	B	`conf`	Automatic Bit- and Memory-Precise Verification of eBPF Code. LPAR Martin Bromberger, Simon Schwarz, Christoph Weidenbach
2024	—	`conf`	First-Order Automatic Literal Model Generation. IJCAR (1) Martin Bromberger, Florent Krasnopol, Sibylle Möhle, Christoph Weidenbach
2024	J	`jnl`	Non-Ground Congruence Closure. CoRR Hendrik Leidinger, Christoph Weidenbach
2023	A	`conf`	An Isabelle/HOL Formalization of the SCL(FOL) Calculus. CADE Martin Bromberger, Martin Desharnais, Christoph Weidenbach
2023	B	`conf`	Exploring Partial Models with SCL. LPAR Martin Bromberger, Simon Schwarz, Christoph Weidenbach
2023	—	`conf`	KBO Constraint Solving Revisited. FroCoS Yasmine Briefs, Hendrik Leidinger, Christoph Weidenbach
2023	J	`jnl`	SCL(EQ): SCL for First-Order Logic with Equality. J. Autom. Reason. Hendrik Leidinger, Christoph Weidenbach
2023	A	`conf`	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. CADE Martin Bromberger, Chaahat Jain, Christoph Weidenbach
2023	J	`jnl`	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. CoRR Martin Bromberger, Chaahat Jain, Christoph Weidenbach
2023	J	`jnl`	SCL(FOL) Revisited. CoRR Martin Bromberger, Simon Schwarz, Christoph Weidenbach
2023	—	`conf`	Symbolic Model Construction for Saturated Constrained Horn Clauses. FroCoS Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
2023	J	`jnl`	Symbolic Model Construction for Saturated Constrained Horn Clauses. CoRR Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
2022	J	`jnl`	A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column. J. Autom. Reason. Sophie Tourret, Christoph Weidenbach
2022	—	`conf`	A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. TACAS (1) Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K. Murali, Christoph Weidenbach
2022	J	`jnl`	A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. CoRR Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K. Murali, Christoph Weidenbach
2022	—	`conf`	A Two-Watched Literal Scheme for First-Order Logic. PAAR@IJCAR Martin Bromberger, Tobias Gehl, Lorenz Leutgeb, Christoph Weidenbach
2022	A	`conf`	An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. IJCAR Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
2022	A	`conf`	Connection-Minimal Abduction in IJCAR Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
2022	—	`conf`	Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract). Description Logics Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
2022	J	`jnl`	Connection-minimal Abduction in EL via Translation to FOL - Technical Report. CoRR Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
2022	—	`conf`	Exploring Partial Models with SCL. PAAR@IJCAR Martin Bromberger, Simon Schwarz, Christoph Weidenbach
2022	A	`conf`	SCL(EQ): SCL for First-Order Logic with Equality. IJCAR Hendrik Leidinger, Christoph Weidenbach
2022	J	`jnl`	SCL(EQ): SCL for First-Order Logic with Equality. CoRR Hendrik Leidinger, Christoph Weidenbach
2022	A	`conf`	Semantic Relevance. IJCAR Fajar Haifani, Christoph Weidenbach
2021	—	`conf`	A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. FroCoS Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach
2021	J	`jnl`	A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. CoRR Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach
2021	B	`conf`	Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. VMCAI Martin Bromberger, Alberto Fiori, Christoph Weidenbach
2021	A	`conf`	Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. CADE Fajar Haifani, Sophie Tourret, Christoph Weidenbach
2020	B	`conf`	A Verified SAT Solver Framework including Optimization and Partial Valuations. LPAR Mathias Fleury, Christoph Weidenbach
2020	J	`jnl`	A complete and terminating approach to linear integer solving. J. Symb. Comput. Martin Bromberger, Thomas Sturm, Christoph Weidenbach
2020	—	`conf`	On a Notion of Relevance. Description Logics Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach
2020	J	`jnl`	Preface to the Special Issue on Automated Reasoning Systems. J. Autom. Reason. Armin Biere, Cesare Tinelli, Christoph Weidenbach
2020	J	`jnl`	SCL with Theory Constraints. CoRR Alberto Fiori, Christoph Weidenbach
2020	J	`jnl`	SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment. J. Autom. Reason. Andreas Teucke, Christoph Weidenbach
2020	—	`conf`	Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification. ISoLA (2) Rasha Faqeh, Christof Fetzer, Holger Hermanns, Jörg Hoffmann, Michaela Klauck, Maximilian A. Köhl, Marcel Steinmetz, Christoph Weidenbach
2019	—	`conf`	On the Expressivity and Applicability of Model Representation Formalisms. FroCos Andreas Teucke, Marco Voigt, Christoph Weidenbach
2019	J	`jnl`	On the Expressivity and Applicability of Model Representation Formalisms. CoRR Andreas Teucke, Marco Voigt, Christoph Weidenbach
2019	A	`conf`	SCL Clause Learning from Simple Models. CADE Alberto Fiori, Christoph Weidenbach
2019	A	`conf`	SPASS-SATT - A CDCL(LA) Solver. CADE Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach
2019	—	`conf`	The Challenge of Unifying Semantic and Syntactic Inference Restrictions. ARCADE@CADE Christoph Weidenbach
2018	J	`jnl`	A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
2018	J	`jnl`	A machine-checked correctness proof for Pastry. Sci. Comput. Program. Noran Azmy, Stephan Merz, Christoph Weidenbach
2017	A*	`conf`	A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAI Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
2017	J	`jnl`	BDI: a new decidable clause class. J. Log. Comput. Manuel Lamotte-Schubert, Christoph Weidenbach
2017	A	`conf`	Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. CADE Andreas Teucke, Christoph Weidenbach
2017	J	`jnl`	Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. CoRR Andreas Teucke, Christoph Weidenbach
2017	—	`conf`	Do Portfolio Solvers Harm? ARCADE@CADE Christoph Weidenbach
2017	J	`jnl`	New techniques for linear arithmetic: cubes and equalities. Formal Methods Syst. Des. Martin Bromberger, Christoph Weidenbach
2017	A	`conf`	On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. CADE Matthias Horbach, Marco Voigt, Christoph Weidenbach
2017	J	`jnl`	On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. CoRR Matthias Horbach, Marco Voigt, Christoph Weidenbach
2017	J	`jnl`	Preface - Special Issue of Selected Extended Papers of IJCAR 2014. J. Autom. Reason. Stéphane Demri, Deepak Kapur, Christoph Weidenbach
2017	J	`jnl`	The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable. CoRR Matthias Horbach, Marco Voigt, Christoph Weidenbach
2016	—	`conf`	A Dynamic Logic for Configuration. ARQNL@IJCAR Ching Hoo Tang, Christoph Weidenbach
2016	C	`conf`	A Rigorous Correctness Proof for Pastry. ABZ Noran Azmy, Stephan Merz, Christoph Weidenbach
2016	A	`conf`	A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAR Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
2016	—	`conf`	Compliance, Functional Safety and Fault Detection by Formal Methods. ISoLA (2) Christof Fetzer, Christoph Weidenbach, Patrick Wischnewski
2016	—	`conf`	Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. SMT@IJCAR Martin Bromberger, Christoph Weidenbach
2016	A*	`conf`	Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. LICS Thomas Sturm, Marco Voigt, Christoph Weidenbach
2016	A	`conf`	Fast Cube Tests for LIA Constraint Solving. IJCAR Martin Bromberger, Christoph Weidenbach
2016	—	`conf`	Ordered Resolution with Straight Dismatching Constraints. PAAR@IJCAR Andreas Teucke, Christoph Weidenbach
2015	—	`conf`	Automated Reasoning Building Blocks. Correct System Design Christoph Weidenbach
2015	J	`jnl`	Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. CoRR Marco Voigt, Christoph Weidenbach
2015	J	`jnl`	Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. CoRR Thomas Sturm, Marco Voigt, Christoph Weidenbach
2015	—	`conf`	First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation. FroCos Andreas Teucke, Christoph Weidenbach
2015	J	`jnl`	First-Order Logic Theorem Proving via Counterexample-Guided Abstraction Refinement. CoRR Andreas Teucke, Christoph Weidenbach
2015	J	`jnl`	Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). Dagstuhl Reports Nikolaj S. Bjørner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, Christoph Weidenbach
2015	A	`conf`	Linear Integer Arithmetic Revisited. CADE Martin Bromberger, Thomas Sturm, Christoph Weidenbach
2015	J	`jnl`	Linear Integer Arithmetic Revisited. CoRR Martin Bromberger, Thomas Sturm, Christoph Weidenbach
2015	—	`conf`	Model-Based Variant Management with v.control. CE Christopher Junk, Robert Rößger, Georg Rock, Karsten Theis, Christoph Weidenbach, Patrick Wischnewski
2015	J	`jnl`	NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper). CoRR Gábor Alagi, Christoph Weidenbach
2015	—	`conf`	NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment. FroCos Gábor Alagi, Christoph Weidenbach
2014	A	`ed.`	Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings IJCAR Stéphane Demri, Deepak Kapur, Christoph Weidenbach
2013	J	`jnl`	Automated Verification of Interactive Rule-Based Configuration Systems (Additional Material). CoRR Deepak Dhungana, Ching Hoo Tang, Christoph Weidenbach, Patrick Wischnewski
2013	A*	`conf`	Automated verification of interactive rule-based configuration systems. ASE Deepak Dhungana, Ching Hoo Tang, Christoph Weidenbach, Patrick Wischnewski
2013	—	`conf`	BDI: A New Decidable First-order Clause Class. LPAR (short papers) Manuel Lamotte-Schubert, Christoph Weidenbach
2013	A	`conf`	Computing Tiny Clause Normal Forms. CADE Noran Azmy, Christoph Weidenbach
2013	J	`jnl`	Deduction and Arithmetic (Dagstuhl Seminar 13411). Dagstuhl Reports Nikolaj S. Bjørner, Reiner Hähnle, Tobias Nipkow, Christoph Weidenbach
2013	—	`conf`	From Search to Computation: Redundancy Criteria and Simplification at Work. Programming Logics Thomas Hillenbrand, Ruzica Piskac, Uwe Waldmann, Christoph Weidenbach
2013	—	`conf`	Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm
2013	—	`ed.`	Programming Logics - Essays in Memory of Harald Ganzinger Programming Logics Andrei Voronkov, Christoph Weidenbach
2013	—	`conf`	Superposition for Bounded Domains. Automated Reasoning and Mathematics Thomas Hillenbrand, Christoph Weidenbach
2012	A	`conf`	A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. IJCAR Martin Suda, Christoph Weidenbach
2012	B	`conf`	Automatic Generation of Invariants for Circular Derivations in SUP(LA). LPAR Arnaud Fietzke, Evgeny Kruglov, Christoph Weidenbach
2012	A	`conf`	Combination of Disjoint Theories: Beyond Decidability. IJCAR Pascal Fontaine, Stephan Merz, Christoph Weidenbach
2012	B	`conf`	Labelled Superposition for PLTL. LPAR Martin Suda, Christoph Weidenbach
2012	B	`conf`	More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. ITP Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach
2012	—	`conf`	Satisfiability Checking and Query Answering for Large Ontologies. PAAR@IJCAR Christoph Weidenbach, Patrick Wischnewski
2012	J	`jnl`	Superposition Decides the First-Order Logic Fragment Over Ground Theories. Math. Comput. Sci. Evgeny Kruglov, Christoph Weidenbach
2012	J	`jnl`	Superposition as a Decision Procedure for Timed Automata. Math. Comput. Sci. Arnaud Fietzke, Christoph Weidenbach
2011	—	`conf`	Superposition Modulo Non-linear Arithmetic. FroCoS Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach
2011	—	`conf`	Towards Verification of the Pastry Protocol Using TLA FMOODS/FORTE Tianxiang Lu, Stephan Merz, Christoph Weidenbach
2010	A	`conf`	On the Saturation of YAGO. IJCAR Martin Suda, Christoph Weidenbach, Patrick Wischnewski
2010	J	`jnl`	Subterm contextual rewriting. AI Commun. Christoph Weidenbach, Patrick Wischnewski
2010	J	`jnl`	Superposition for fixed domains. ACM Trans. Comput. Log. Matthias Horbach, Christoph Weidenbach
2010	—	`conf`	Superposition-Based Analysis of First-Order Probabilistic Timed Automata. LPAR (Yogyakarta) Arnaud Fietzke, Holger Hermanns, Christoph Weidenbach
2009	—	`conf`	Analysis of Authorizations in SAP R/3. FTP Manuel Lamotte-Schubert, Christoph Weidenbach
2009	A	`conf`	Decidability Results for Saturation-Based Model Building. CADE Matthias Horbach, Christoph Weidenbach
2009	B	`conf`	Deciding the Inductive Validity of FOR ALL THERE EXISTS CSL Matthias Horbach, Christoph Weidenbach
2009	J	`jnl`	Labelled splitting. Ann. Math. Artif. Intell. Arnaud Fietzke, Christoph Weidenbach
2009	A	`conf`	SPASS Version 3.5. CADE Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski
2009	—	`conf`	Superposition Modulo Linear Arithmetic SUP(LA). FroCoS Ernst Althaus, Evgeny Kruglov, Christoph Weidenbach
2008	—	`conf`	Contextual Rewriting in SPASS. PAAR/ESHOL Christoph Weidenbach, Patrick Wischnewski
2008	A	`conf`	Labelled Splitting. IJCAR Arnaud Fietzke, Christoph Weidenbach
2008	J	`jnl`	Superposition for Fixed Domains CoRR Matthias Horbach, Christoph Weidenbach
2008	B	`conf`	Superposition for Fixed Domains. CSL Matthias Horbach, Christoph Weidenbach
2007	A	`conf`	Labelled Clauses. CADE Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv
2007	A	`conf`	System Description: SpassVersion 3.0. CADE Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic
2002	A	`conf`	S PASS Version 2.0. CADE Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobalt, Dalibor Topic
2001	—	`ch.`	Combining Superposition, Sorts and Splitting. Handbook of Automated Reasoning Christoph Weidenbach
2001	—	`ch.`	Computing Small Clause Normal Forms. Handbook of Automated Reasoning Andreas Nonnengart, Christoph Weidenbach
2001	B	`conf`	First-Order Atom Definitions Extended. LPAR Bijan Afshordel, Thomas Hillenbrand, Christoph Weidenbach
1999	—	`conf`	MSPASS: Subsumption Testing with SPASS. Description Logics Ullrich Hustadt, Renate A. Schmidt, Christoph Weidenbach
1999	A	`conf`	System Description: Spass Version 1.0.0. CADE Christoph Weidenbach
1999	A	`conf`	Towards an Automatic Analysis of Security Protocols in First-Order Logic. CADE Christoph Weidenbach
1998	A	`conf`	On Generating Small Clause Normal Forms. CADE Andreas Nonnengart, Georg Rock, Christoph Weidenbach
1998	J	`jnl`	Paradigmen und Perspektiven der automatischen Deduktion. Künstliche Intell. Reinhold Letz, Christoph Weidenbach
1998	—	`conf`	Unification in Extension of Shallow Equational Theories. RTA Florent Jacquemard, Christoph Meyer, Christoph Weidenbach
1997	J	`jnl`	SPASS - Version 0.49. J. Autom. Reason. Christoph Weidenbach
1997	A	`conf`	Soft Typing for Ordered Resolution. CADE Harald Ganzinger, Christoph Meyer, Christoph Weidenbach
1996	—	`—`	Computational aspects of a first-order logic with sorts. Christoph Weidenbach
1996	A	`conf`	SPASS & FLOTTER Version 0.42. CADE Christoph Weidenbach, Bernd Gaede, Georg Rock
1996	A	`conf`	Unification in Pseudo-Linear Sort Theories is Decidable. CADE Christoph Weidenbach
1996	J	`jnl`	Unification in Sort Theories and Its Applications. Ann. Math. Artif. Intell. Christoph Weidenbach
1995	J	`jnl`	A Note on Assumptions about Skolem Functions. J. Autom. Reason. Hans Jürgen Ohlbach, Christoph Weidenbach
1995	J	`jnl`	First-Order Tableaux with Sorts. Log. J. IGPL Christoph Weidenbach
1993	A*	`conf`	Extending the Resolution Method with Sorts. IJCAI Christoph Weidenbach
1992	—	`conf`	A New Sorted Logic. GWAI Christoph Weidenbach
1992	J	`jnl`	Deduktionssysteme. Künstliche Intell. Manfred Kerber, Christoph Weidenbach
1990	A	`conf`	A Resolution Calculus with Dynamic Sort Structures and Partial Functions. ECAI Christoph Weidenbach, Hans Jürgen Ohlbach