| Time | Title | Speaker |
|---|
| 09:00 - 09:05 |
the organizers |
Opening |
| 09:05 - 10:30 |
Session I |
Michael Kohlhase (chair) |
| 09:05 - 10:05 |
Laurent Vigneron |
Automatic Verification of Security Protocols |
| 10:05 - 10:30 |
Yannick Chevalier |
A Simple Constraint Solving
Procedure for Protocols with Exclusive Or |
| 10:30 - 11:00 |
Coffee Break |
| 11:10 - 12:25 |
Session II |
Ralf Treinen (chair) |
| 11:10 - 11:35 |
Stephanie Delaune and Florent Jacquemard |
Narrowing Based Constraint Solving
for the Verification of Security Protocols |
| 11:35 - 12:00 |
Calogero Zarba |
A Quantifier Elimination Algorithm for
a Fragment of Set Theory Involving the Cardinality Operator |
| 12:00- 12:25 |
Marco Alberti and Evelina Lamma |
Inference with Arbitrarily
Quantified Variables |
| 12:25 - 14:00 |
Lunch |
| 14:00 - 15:40 |
Session III |
Manfred Schmidt-Schauß (chair) |
| 14:00 - 14:25 |
Javier Alvez and Paqui Lucio |
Equational Constraint Solving using
Quasi-solved Forms? |
| 14:25 - 14:50 |
Lilia Georgieva |
Intelligent backtracking
techniques for resolution decision procedures |
| 14:50 - 15:15 |
Stephane Le Roux and Pierre Lescanne |
Solving Equations in a Language
With Control Operators |
| 15:15 - 15:40 |
Bahareh Badban, Jaco van de Pol, Olga Tveretina, Hans Zantema, |
Solving Satisfiability of Ground
Term Algebras Using DPLL and Unification? |
| 15:40 - 16:10 |
Coffee Break |
| 16:10 - 17:25 |
Session IV |
Franz Baader (chair) |
| 16:10 - 16:35 |
Temur Kutsia and Mircea Marin |
Unification Procedure for Terms
with Sequence Variables and Sequence Functions |
| 16:35 - 17:00 |
Martin Plümicke |
Type Unification in Generic-Java |
| 17:00 - 17:25 |
Joseph Goguen and Monica Marcus |
Scritical Pairs and
Sunification (talk given by Laurent Vigneron) |
| 17:30 - 18:00 |
UNIF business meeting |