Automation of Logic
English

Christoph Weidenbach

Prof. Dr. Christoph Weidenbach

Head of research group

Automation of Logic

Head of the research areas

First-Order Theorem Proving
Decidable Fragments
Automated Verification

Short CV

 

Max-Planck-Institute for Informatics
Saarland Informatics Campus E1 4
66123 Saarbrücken

+49 681 9325-2900, fax -2999

weidenbach@mpi-inf.mpg.de

 

Physical address: building E1 5, room 612

Research Interests

  • Automated Deduction
  • Decision Procedures
  • Theorem Proving
  • Combination of Theories
  • Combination of Systems

Selected Publications

  • Bromberger, M., Fiori, A. and Weidenbach, C., 2021, Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. in VMCAI 2021, pp. 511–533.
  • Azmy, N., Merz, S. and Weidenbach, C., 2016, A Rigorous Correctness Proof for Pastry. in 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2016, pp. 86-101.
  • Blanchette, J. C., Fleury, M. and Weidenbach, C., 2016, A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. in 8th International Joint Conference on Automated Reasoning, IJCAR 2016, pp. 25-44.
  • Bromberger, M. and Weidenbach, C., 2016, Fast Cube Tests for LIA Constraint Solving. in 8th International Joint Conference on Automated Reasoning, IJCAR 2016, pp. 116-132.
  • Fetzer, C., Weidenbach, C. and Wischnewski, P., 2016, Compliance, Functional Safety and Fault Detection by Formal Methods. in 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, ISoLA 2016, pp. 626-632.
  • Sturm, T., Voigt, M. and Weidenbach, C., 2016, Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. in 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 86-95.
  • Weidenbach, C., 2015, Automated Reasoning Building Blocks. in Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, pp. 172-188.
  • 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.
  • 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., 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.
  • Fietzke, A. and Weidenbach, C., 2008, Labelled Splitting in 4th International Joint Conference on Automated Reasoning, IJCAR 2008, LNCS 5195, pp. 459-474.
  • 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

Teaching

List of courses / current teaching activities

List of courses / past teaching activities

Activities

  • Founded the startup Logic4Business
  • Editor of the Journal of Automated Reasoning
  • Chairman of Steering Committee BWINF

Employment

  • 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

Education