The
MaxPlanck 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).
Programme:
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 BachmairGanzinger Models
 Nachum Dershowitz (and Maria Paola Bonacina)
Canonical Ground Horn Theories
 Robert Nieuwenhuis
Firstorder 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 SofronieStokkermans
On reasoning in local theory extensions

16:45  17:45 
 Renate Schmidt
FirstOrder Resolution Methods for Modal Logics
 Witold Charatonik
Set constraints

18h 
 Commemoration of Harald Ganzinger

19h 

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 
 JeanPierre 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
BioLogics: 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



Hotels:
We recommend
If you need help, e.g., for reserving a hotel, please contact
Brigitta Hansen
<hansen@mpisb.mpg.de>.