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).
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 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
|
| 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 |
- 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
|
|
|
|
Hotels:
We recommend
If you need help, e.g., for reserving a hotel, please contact Brigitta Hansen <hansen@mpi-sb.mpg.de>.