J. Tapken (Univ. Oldenburg): Implementing hierarchical graph-structures

V. Nepomniaschy (Russian Academy of Sciences, Novosibirsk): Verification of definite iteration over hierarchical data structures

K. Lano (Imperial College, London), A. Evans (Univ. York): Rigorous development in UML

C. L\"uth, H. Tej, Kolyang, B. Krieg-Brueckner (Univ. Bremen), tool demo: TAS and IsaWin: Tools for transformational program development and theorem proving

M. Huhn (Univ. Karlsruhe), P. Niebert (Univ. Hildesheim), F. Wallner (TU Munich): Model checking logics for communicating agents

M. Narasimha (North Carolina State University), R. Cleaveland (SUNY at Stony Brook), P. Iyer (North Carolina State University): Probabilistic temporal logics via the modal mu-calculus

A. Muscholl (Univ. Stuttgart): Matching specifications for message sequence charts

C. Bodei, P. Degano (Univ. Pisa), F. Nielson, H. Riis Nielson (Aarhus University): Static analysis of processes for no read-up and no write-down

C. Viho (IRISA/IFSIC, Rennes), H. Kahlouche (INRIA, Rennes), M. Zendri (Bull R&D): Hardware testing using a communication protocol conformance testing tool

C. Kern, T. Ono-Tesfaye, M. Greenstreet (Univ. British Columbia): A light-weight framework for hardware verification

D. Peters (Memorial Univ. of Newfoundland and McMaster University), D.L. Parnas (McMaster University): An easily extensible toolset for tabular mathematical expressions

J. Knoop (Univ. Dortmund): From DFA-frameworks to DFA-generators: A unifying multiparadigm approach

M. M\"uller-Olm, B. Steffen (Univ. Dortmund), R. Cleaveland (SUNY, Stony Brook): On the evolution of reactive components: A process-algebraic approach

T. Nipkow and L. Nieto (TU Munich): Owicki/Gries in Isabelle/HOL

R. Bruni (Univ. Pisa), J. Meseguer (SRI International, Menlo Park), U. Montanari (Univ. Pisa): Executable tile specifications for process calculi

E. Coscia, G. Reggio (Univ. Genova): JTN: A Java-targeted graphic formal notation for reactive and concurrent systems

R. Arruabarrena, P. Lucio, M. Navarro (Univ. San-Sebastian): A strong logic programming view for static embedded implications

M. Lenisa (Univ. Udine): A coinductive logical system for bisimulation equivalence on circular objects

F.S de Boer (Utrecht University): A WP-calculus for OO

D. Spelt, S. Even (Univ. Twente): A theorem prover-based analysis tool for object-oriented databases

R. Smeliansky, A. Bakhmurov, A. Kapitonova (Moscow State University): DYANA: An environment for embedded system design and analysis

E. Gunter, D. Peled (Bell Laboratories): Path exploration tool

P. Buchholz, P. Kemper (Univ. Dortmund): Modular state level analysis of distributed systems - techniques and tool support

18:00