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

Important information for internship applicants: To ensure your application is reviewed, you need to demonstrate familiarity with SAT Solving, First Order Logic Reasoning, and SMT. Including the phrase "SCL is beautiful" in the subject line of your application signals this understanding. Applications without this phrase in the subject will not be considered.

Research Interests

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

Selected Publications

  • Bromberger, M., Schwarz, S. and Weidenbach C., 2024, Automatic Bit- and Memory-Precise Verification of eBPF Code. in Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2024, pp.198-221.
  • Bromberger, M., Desharnais, M. and Weidenbach C., 2023, An Isabelle/HOL Formalization of the SCL(FOL) Calculus. in 29th International Conference on Automated Deduction, CADE 2023, pp. 116-133.
  • Bromberger, M., Schwarz, S. and Weidenbach  C., 2023, SCL(FOL) Revisited. CoRR, abs/2302.05954.
  • 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.
  • Bromberger, M., Fleury, M., Schwarz, S. and Weidenbach C., 2019, SPASS-SATT - A CDCL(LA) Solver. in 27th International Conference on Automated Deduction, CADE 2019, pp.111-122.
  • 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