Christoph Weidenbach

According to our database1, Christoph Weidenbach authored at least 75 papers between 1990 and 2018.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

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. Reasoning, 2018

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

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

New techniques for linear arithmetic: cubes and equalities.
Formal Methods in System Design, 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 Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality.
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

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

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.
Mathematics in Computer Science, 2012

Superposition as a Decision Procedure for Timed Automata.
Mathematics in Computer Science, 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 + .
Proceedings of the Formal Techniques for Distributed Systems, 2011

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
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 * 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
Superposition for Fixed Domains.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

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

Labelled Splitting.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 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.
KI, 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. Reasoning, 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. Reasoning, 1995

First-Order Tableaux with Sorts.
Logic Journal of the 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.
KI, 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...