Bologna, Italy, July 11-12, 1997

- Faron Moller:
**Preface.**

- Felice Balarin:
**Verifying invariants by approximate image computation.**

- Zakaria Bouziane, Alain Finkel:
**Cyclic Petri net reachability sets are semi-linear effectively constructible.**

- Olaf Burkart:
**Model checking rationally restricted right closures of recognizable graphs.**

- Dennis Dams, Rob Gerth:
**The bounded retransmission protocol revisited.**

- Alain Finkel, Bernard Willems, Pierre Wolper:
**A direct symbolic approach to model checking pushdown systems.**

- Laurent Fribourg, Hans Olsén:
**Reachability sets of parameterized rings as regular languages.**

- Petr Jancar, Antonín Kucera:
**Bisimilarity of processes with finite-state systems.**

- David Lesens, Hassen Saïdi:
**Abstraction of parameterized networks.**

- Géraud Sénizergues:
**L(A) = L(B)?**

- Jitka Stríbrná:
**Decidability of strong bisimulation of basic parallel processes using Hilbert's basis theorem.**