Homepage
Christoph Weidenbach
Max-Planck-Institut für Informatik
Research Leader
Research Coordination
Campus E1 4, Room 612 (Building E1 5)
66123 Saarbrücken
Germany
Email:
Get my email address via email
Phone: +49 681 9325 2900
Fax: +49 681 9325 2999
- Automated Deduction
- Decision Procedures
- Theorem Proving
- Combination of Theories
- Combination of Systems
- Fontaine, P., Merz, S. and Weidenbach, C., 2012,
Combination of Disjoint Theories: Beyond Decidability. in 6th International Joint Conference on Automated Reasoning, IJCAR 2012, pp. 256-270.
- Suda, M. and Weidenbach, C., 2012,
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. in 6th International Joint Conference on Automated Reasoning, IJCAR 2012, pp. 537-543.
- Blanchette J. C., Popescu, A., Wand, D. and Weidenbach, C., 2012,
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. in Third International Conference on Interactive Theorem Proving, ITP 2012, pp. 345-360.
- Fietzke, A., Kruglov, E. and Weidenbach, C., 2012,
Automatic Generation of Invariants for Circular Derivations in SUP(LA). in 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2012, pp. 197-211.
- Suda, M. and Weidenbach, C., 2012,
Labelled Superposition for PLTL. in 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2012, pp. 391-405.
- Lu, T., Merz, S. and Weidenbach, C., 2010,
Model Checking the Pastry Routing Protocol. in 10th International Workshop Automatic Verification of Critical Systems, AVOCS 2010, pp. 19-21.
- Suda, M., Weidenbach, C. and Wischnewski, P., 2010,
On the Saturation of YAGO. in 5th International Joint Conference on Automated Reasoning, IJCAR 2010, LNCS 6173, pp. 441-456.
- Horbach, M. and Weidenbach, C., 2010,
Superposition for Fixed Domains. ACM Transactions on Computational Logic, Vol. 11, pp.1-27.
- Weidenbach C., Dimova D., Fietzke A., Kumar R., Suda M. and Wischnewski P., 2009,
SPASS Version 3.5. in 22nd International Conference on Automated Deduction, CADE 2009, LNCS 5663, pp. 140-145.
- Althaus, E., Kruglov E. and Weidenbach C., 2009,
Superposition Modulo Linear Arithmetic SUP(LA) in 7th international Symposium on Frontiers of Combining Systems, FroCos 2009, LNCS 5749, pp. 84-99.
- Fietzke, A. and Weidenbach, C., 2008,
Labelled Splitting in 4th International Joint Conference on Automated Reasoning, IJCAR 2008, LNCS 5195, pp. 459-474.
- Lev-Ami, T., Weidenbach, C., Reps, T. and Sagiv, M. 2007,
Labelled Clauses
in 21st International Conference on Automated Deduction, CADE-21, LNCS 4603, pp. 311-327.
- Hillenbrand, T. and Weidenbach, C., 2007,
Superposition for Finite Domains,
Research Report, Max Planck Institute for Informatics, Saarbrücken, MPI-I-2007-RG1-002.
- Nonnengart, A. and Weidenbach, C., 2001,
Computing Small Clause Normal Forms
in A. Robinson and A. Voronkov, editors, Handbook of
Automated Reasoning, Elsevier, Chapter 6, pp. 335-367.
- Weidenbach, C., 2001,
Combining Superposition, Sorts and Splitting
in A. Robinson and A. Voronkov, editors, Handbook of
Automated Reasoning, Elsevier, Chapter 27, pp. 1965-2012.
- Weidenbach, C., 1999, Towards an Automatic Analysis of Security Protocols in
H. Ganzinger, editor, 16th International Conference on Automated Deduction, CADE-16,
Vol. 1632 of LNAI,
Springer, pp. 378-382.
- Jacquemard F., Meyer C. and Weidenbach C., 1998
Unification in Extensions of Shallow Equational Theories in
T. Nipkow, editor, Rewriting Techniques and Applications,
9th International Conference, RTA-98,
Vol. 1379 of LNCS,
Springer, pp. 76-90.
- Ganzinger, H., Meyer, C. and Weidenbach C., 1997,
Soft Typing for Ordered Resolution in
W. McCune, editor, 14th International Conference on Automated Deduction, CADE-14,
Vol. 1249 of LNAI,
Springer, pp. 321-335.
All Publications of Christoph Weidenbach
List of courses / current teaching activities
List of courses / past teaching activities
- 1996-1999 Five championships by SPASS
in the CADE system competitions.
- 2005- Research Leader of the independant research group Automation of Logic at the Max-Planck-Institute for Informatics
- 2005- Research Coordinator at the Max-Planck-Institute for Informatics
- 1999-2005 IT Manager GM Powertrain Europe
- 1991-1999 Researcher at the Max-Planck-Institute for Informatics
- 1989-1991 Researcher at the University Kaiserslautern