Christoph Weidenbach

Orcid: 0000-0001-6002-0458

Affiliations:
  • Max Planck Institute for Informatics, Saarbrücken, Germany


According to our database1, Christoph Weidenbach authored at least 110 papers between 1990 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Automatic Bit- and Memory-Precise Verification of eBPF Code.
Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

First-Order Automatic Literal Model Generation.
Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

2023
SCL(EQ): SCL for First-Order Logic with Equality.
J. Autom. Reason., September, 2023

SCL(FOL) Revisited.
CoRR, 2023

Exploring Partial Models with SCL.
Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Symbolic Model Construction for Saturated Constrained Horn Clauses.
Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

KBO Constraint Solving Revisited.
Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning.
Proceedings of the Automated Deduction - CADE 29, 2023

An Isabelle/HOL Formalization of the SCL(FOL) Calculus.
Proceedings of the Automated Deduction - CADE 29, 2023

2022
A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column.
J. Autom. Reason., 2022

Connection-minimal Abduction in EL via Translation to FOL - Technical Report.
CoRR, 2022

A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

A Two-Watched Literal Scheme for First-Order Logic.
Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract).
Proceedings of the 35th International Workshop on Description Logics (DL 2022) co-located with Federated Logic Conference (FLoC 2022), 2022

Semantic Relevance.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Connection-Minimal Abduction in <i>EL</i> via Translation to FOL.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

An Efficient Subsumption Test Pipeline for BS(LRA) Clauses.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic.
Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance.
Proceedings of the Automated Deduction - CADE 28, 2021

2020
A complete and terminating approach to linear integer solving.
J. Symb. Comput., 2020

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment.
J. Autom. Reason., 2020

Preface to the Special Issue on Automated Reasoning Systems.
J. Autom. Reason., 2020

SCL with Theory Constraints.
CoRR, 2020

A Verified SAT Solver Framework including Optimization and Partial Valuations.
Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles, 2020

On a Notion of Relevance.
Proceedings of the 33rd International Workshop on Description Logics (DL 2020) co-located with the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), 2020

2019
The Challenge of Unifying Semantic and Syntactic Inference Restrictions.
Proceedings of the Second International Workshop on Automated Reasoning: Challenges, 2019

On the Expressivity and Applicability of Model Representation Formalisms.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

SCL Clause Learning from Simple Models.
Proceedings of the Automated Deduction - CADE 27, 2019

SPASS-SATT - A CDCL(LA) Solver.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
A machine-checked correctness proof for Pastry.
Sci. Comput. Program., 2018

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
J. Autom. Reason., 2018

2017
BDI: a new decidable clause class.
J. Log. Comput., 2017

Preface - Special Issue of Selected Extended Papers of IJCAR 2014.
J. Autom. Reason., 2017

New techniques for linear arithmetic: cubes and equalities.
Formal Methods Syst. Des., 2017

The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable.
CoRR, 2017

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

Do Portfolio Solvers Harm?
Proceedings of the ARCADE 2017, 2017

Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints.
Proceedings of the Automated Deduction - CADE 26, 2017

On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Compliance, Functional Safety and Fault Detection by Formal Methods.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Ordered Resolution with Straight Dismatching Constraints.
Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), 2016

A Dynamic Logic for Configuration.
Proceedings of the 2nd International Workshop Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)., 2016

Computing a Complete Basis for Equalities Implied by a System of LRA Constraints.
Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, 2016

Fast Cube Tests for LIA Constraint Solving.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

A Rigorous Correctness Proof for Pastry.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

2015
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381).
Dagstuhl Reports, 2015

Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete.
CoRR, 2015

First-Order Logic Theorem Proving via Counterexample-Guided Abstraction Refinement.
CoRR, 2015

NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper).
CoRR, 2015

Model-Based Variant Management with v.control.
Proceedings of the Transdisciplinary Lifecycle Analysis of Systems, 2015

First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Linear Integer Arithmetic Revisited.
Proceedings of the Automated Deduction - CADE-25, 2015

Automated Reasoning Building Blocks.
Proceedings of the Correct System Design, 2015

2013
Deduction and Arithmetic (Dagstuhl Seminar 13411).
Dagstuhl Reports, 2013

Automated Verification of Interactive Rule-Based Configuration Systems (Additional Material).
CoRR, 2013

BDI: A New Decidable First-order Clause Class.
Proceedings of the LPAR 2013, 2013

Automated verification of interactive rule-based configuration systems.
Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

Computing Tiny Clause Normal Forms.
Proceedings of the Automated Deduction - CADE-24, 2013

Harald Ganzinger's Legacy: Contributions to Logics and Programming.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

Superposition for Bounded Domains.
Proceedings of the Automated Reasoning and Mathematics, 2013

From Search to Computation: Redundancy Criteria and Simplification at Work.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012
Superposition Decides the First-Order Logic Fragment Over Ground Theories.
Math. Comput. Sci., 2012

Superposition as a Decision Procedure for Timed Automata.
Math. Comput. Sci., 2012

Labelled Superposition for PLTL.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Automatic Generation of Invariants for Circular Derivations in SUP(LA).
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Satisfiability Checking and Query Answering for Large Ontologies.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Combination of Disjoint Theories: Beyond Decidability.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011
Superposition Modulo Non-linear Arithmetic.
Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Towards Verification of the Pastry Protocol Using TLA<sup> + </sup>.
Proceedings of the Formal Techniques for Distributed Systems, 2011

2010
Superposition for fixed domains.
ACM Trans. Comput. Log., 2010

Subterm contextual rewriting.
AI Commun., 2010

Superposition-Based Analysis of First-Order Probabilistic Timed Automata.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

On the Saturation of YAGO.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
Labelled splitting.
Ann. Math. Artif. Intell., 2009

Analysis of Authorizations in SAP R/3.
Proceedings of the 7th International Workshop on First-Order Theorem Proving, 2009

Superposition Modulo Linear Arithmetic SUP(LA).
Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

Deciding the Inductive Validity of FOR ALL THERE EXISTS <sup>*</sup> Queries.
Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

SPASS Version 3.5.
Proceedings of the Automated Deduction, 2009

Decidability Results for Saturation-Based Model Building.
Proceedings of the Automated Deduction, 2009

2008
Contextual Rewriting in SPASS.
Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, 2008

2007
System Description: SpassVersion 3.0.
Proceedings of the Automated Deduction, 2007

Labelled Clauses.
Proceedings of the Automated Deduction, 2007

2002
S PASS Version 2.0.
Proceedings of the Automated Deduction, 2002

2001
First-Order Atom Definitions Extended.
Proceedings of the Logic for Programming, 2001

Combining Superposition, Sorts and Splitting.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Computing Small Clause Normal Forms.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

1999
MSPASS: Subsumption Testing with SPASS.
Proceedings of the 1999 International Workshop on Description Logics (DL'99), Linköping, Sweden, July 30, 1999

System Description: Spass Version 1.0.0.
Proceedings of the Automated Deduction, 1999

Towards an Automatic Analysis of Security Protocols in First-Order Logic.
Proceedings of the Automated Deduction, 1999

1998
Paradigmen und Perspektiven der automatischen Deduktion.
Künstliche Intell., 1998

Unification in Extension of Shallow Equational Theories.
Proceedings of the Rewriting Techniques and Applications, 9th International Conference, 1998

On Generating Small Clause Normal Forms.
Proceedings of the Automated Deduction, 1998

1997
SPASS - Version 0.49.
J. Autom. Reason., 1997

Soft Typing for Ordered Resolution.
Proceedings of the Automated Deduction, 1997

1996
Unification in Sort Theories and Its Applications.
Ann. Math. Artif. Intell., 1996

SPASS & FLOTTER Version 0.42.
Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

Unification in Pseudo-Linear Sort Theories is Decidable.
Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

Computational aspects of a first-order logic with sorts.
PhD thesis, 1996

1995
A Note on Assumptions about Skolem Functions.
J. Autom. Reason., 1995

First-Order Tableaux with Sorts.
Log. J. IGPL, 1995

1993
Extending the Resolution Method with Sorts.
Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry, France, August 28, 1993

1992
Deduktionssysteme.
Künstliche Intell., 1992

A New Sorted Logic.
Proceedings of the GWAI-92: Advances in Artificial Intelligence, 16th German Conference on Artificial Intelligence, Bonn, Germany, August 31, 1992

1990
A Resolution Calculus with Dynamic Sort Structures and Partial Functions.
Proceedings of the 9th European Conference on Artificial Intelligence, 1990


  Loading...