The Max-Planck Institute for Informatics and the Department of Computer Science at Saarland University will organize a workshop on Programming Logics to commemorate the life and scientific achievements of Harald Ganzinger on the first anniversary of his sad and untimely death. The programme will include an official commemoration of Harald Ganzinger, and a joint workshop dinner. The workshop will take place in Building 45 (Computer Science Dept.) of Saarland University in Saarbrücken.

Colleagues and friends close to Harald will give talks covering the variety of research areas Harald has worked in. A preliminary programme is attached below.

We are collecting contributions for a Springer LNCS volume in memoriam of Harald Ganzinger; every workshop participant will receive the volume.

The organizers (Andreas Podelski, Andrei Voronkov and Reinhard Wilhelm).


Friday, June 3rd
9:00 - 10:00
  • Opening (Reinhard Wilhelm)
  • Andrei Voronkov (and Roberto Nieuwenhuis)
    The Scientific Life of Harald Ganzinger
10:30 - 12:30
  • Christopher Lynch
    Constructing Bachmair-Ganzinger Models
  • Nachum Dershowitz (and Maria Paola Bonacina)
    Canonical Ground Horn Theories
  • Robert Nieuwenhuis
    First-order theorem proving by constraint propagation and by local search
  • David Plaisted (and Swaha Miller)
    The Relative Power of Semantics and Unification.
13:30 - 15:00
  • Deepak Kapur
    Will Algebraic Geometry Rescue Program Verification?
  • Pierre Lescanne
    Experiments in higher order epistemic logic with common knowledge using a proof assistant.
  • Claude Kirchner, Hélène Kirchner, Fabrice Nahon
    Narrowing based Inductive Proof Search
15:30 - 16:30
  • Uwe Waldmann
    Modular Proof Systems for Partial Functions with Weak Equality
  • Viorica Sofronie-Stokkermans
    On reasoning in local theory extensions
16:45 - 17:45
  • Renate Schmidt
    First-Order Resolution Methods for Modal Logics
  • Witold Charatonik
    Set constraints
  • Commemoration of Harald Ganzinger
Saturday, June 4th
9:00 - 10:00
  • Neil Jones
    Programs as Data Objects [short talk on collaboration with Harald]
  • Manfred Broy
    Reasoning on feedback under lack of time
  • Frank Pfenning
    Linear Logical Algorithms
10:30 - 11:30
  • David McAllester
    Logical Algorithms and Generalized A* in Computer Vision and NLP
  • Moshe Y. Vardi
    Alternation as an Algorithmic Construct
11:45 - 12:45
  • Jean-Pierre Jouannaud (and Jean Goubault)
    Resolution, Paramodulation and Finite Semantics Trees
  • Amir Pnueli
    Program Synthesis in Action: Solving a Doubly Exponential Hard Problem in Time N^3
13:30 - 14:30
  • Robert Giegerich
    The Power of Abstraction in Biosequence Analysis
  • Alexander Bockmayr
    Bio-Logics: Logic modeling of bioregulatory networks
15:00 - 16:30
  • Gernot Stenz (and Reinhold Letz)
    Advanced Pruning Concepts for Tableau Calculi
  • Hans de Nivelle (and Ruzica Piskac)
    Verification of a Result Checker in Saturate
  • Andreas Podelski (and Andrey Rybalchenko)
    Software Model Checking for Termination and Liveness


We recommend

If you need help, e.g., for reserving a hotel, please contact Brigitta Hansen <>.