The development of our modern societies needs more and more involvement of computers in managing highly complex and (safety-)critical tasks, e.g., in telecommunication, chemical and physical process control, transportation systems, etc. It is essential to be able to produce reliable hardware and software systems, since any erroneous behaviour can have catastrophic (economical and human) consequences. This requires rigorous methods and techniques to conceive, analyse and validate these systems.

The verification problem consists in checking whether a system satisfies its specification. During the two last decades, significant achievements have been obtained in the case of finite-state systems (systems with finitely many states). One of the main actual challenges in the domain of automated verification is the conception of methods and tools allowing to deal with verification problems beyond the finite-state framework.

Such problems rise naturally as soon as we consider aspects like:

• real-time constraints: timed and hybrid systems,
• unbounded discrete data structures: counters, fifo-channels, stacks, etc.
• parametric reasoning about families of systems, e.g., networks of processes,
• process mobility, dynamic creation and destruction of processes (dynamic modification of the communication structure).

In the last two years the specification and verification of infinite-state systems have attracted the attention of more and more researchers belonging to a very broad range of research communities. Both process algebras (or term rewriting systems) and automata (or finite control machines) are being used as specification formalisms. Verification problems can be reduced to checking behavioural equivalence or implementation (simulation) relations, or to checking the satisfaction of properties described in temporal logics or fixpoint calculi (model checking problems). Verification methods can be deductive (based on the use of theorem provers), or algorithmic (based on decision or semi-decision procedures). Algorithmic methods can be based on fixpoint theory, automata theory or (constrained) logic programming.

Recent work has shown that different techniques can be combined with sometimes spectacular results. As a result, it is being acknowledged that only a combination of techniques can lead to methods and tools widely used in practice. The aim of this meeting is to bring together researchers working on different research fields in order to make a synthesis on the state of the art and evaluate the potential of combined methods. Concrete questions to be addressed are:

• Which results in logic, automata theory, rewriting systems, etc. are applicable to automatic verification?
• How should deductive and algorithmic techniques be combined?
• Which are the right techniques to deal with abstraction?
• Which are the most promising application fields (mobile systems, cryptographic protocols, static program analysis ...), and which are the most appropriate models, specification formalisms, and verification techniques to deal with them?