IOA is a high-level distributed programming language based on the formal I/O automaton model for asynchronous concurrent systems. A suite of software tools, called the IOA toolkit, has been designed and partially implemented to facilitate the analysis and verification of distributed systems using techniques supported by the formal model. An important proof technique for distributed systems defined by a hierarchy of abstractions involves the notion of a simulation relation between pairs of automata at different levels in the hierarchy. The IOA toolkit's simulator tests purported simulation relations by executing the low-level automaton and, given a proposed correspondence between its steps and those of the higher-level automaton, generating and checking an execution of the higher-level automaton. Once checked by the simulator, the simulation relation and the step correspondence can be used in conjunction with the toolkit's proof tools to construct a formal proof that the low-level automaton implements the higher-level one. This paper presents a case study that illustrates this use of the IOA toolkit to prove correct an algorithm for mutual exclusion. The case study shows how tools like the IOA simulator can play an important role in proving distributed systems correct.

The Model-Checking Kit is a collection of programs which allow to model finite state systems using a variety of modelling languages, and verify them using a variety of checkers, including deadlock-checkers, reachability-checkers, and model-checkers for the temporal logics CTL and LTL.

We present two new facilities of the high level Petri net editor of the PEP tool. The latest version extends the class of supported Petri nets by a time extension of M-nets. Additionally it features a new operator for asynchronous communication complementing the synchronization operator. We present an example of an ARQ protocol with enhanced acknowledgment handling.

CADP\ is a toolbox for specifying and verifying asynchronous finite-state systems described using process algebraic languages. It offers a wide range of state-of-the-art functionalities assisting the user throughout the design process: compilation, rapid prototyping, interactive and guided simulation, verification by equivalence/preorder checking and temporal logic model-checking, and test generation. The languages, models, and verification techniques used in \CADP\ have a broad application domain, allowing to deal with communication protocols, distributed systems, embedded software, mobile telephony, asynchronous hardware, cryptography, security, human-computer interaction, etc. \CADP\ is currently used both in industrial companies and academic institutions for research and teaching purposes. During the last years, over 50 applications and case-studies performed using \CADP\ have been reported.

Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete and the continuous time setting. In this paper, we describe the prototype model checker ETMCC for discrete and continuous-time Markov chains, where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool.

We present a tool that performs verification of quantified reachability properties over Markov decision processes (or probabilistic transition system). The originality of the tool is to provide two reduction techniques that limit the state space explosion problem: automatic abstraction and refinement algorithms, and a so-called essential states reduction. We present several case-studies to illustrate the usefulness of these techniques.

Parallel PV is based on the sequential PV model-checker. Sequential PV is an depth-first LTL-X model-checker for an enhanced subset of the Promela language. Parallel PV is a breadth-first safety-only model-checker. It capitalizes on PV's two-phase partial-order reduction algorithm by carrying out partial order reduction steps with no communication, and performs state space distribution at global steps. This helps reduce the number of messages exchanged. Also, based on state ownership information, parallel PV reduces the number of states that are cached. This reduction is in addition to the selective state caching supported by sequential PV. We report encouraging preliminary experimental results drawn from the domain of `hardware' protocols, as well as software models generated by the Bandera tool. Implementation details of parallel PV and setup information are also provided.

Information resourses on verification tools are of high interest not only to academia and research communities, there is a growing interest from the commercial sector to be expected as well in the near future. Several web sites already provide collective information related to the verification tools. However, most of these resources are out-of-date, not well-structured, difficult to maintain.
Yahoda is a project that aims to overcome at least some of the above mentioned problems. Yahoda is based on a relational database, so as the data can be consistently added/modified/updated. It is the tool developer who actually maintains the information about the tool via an authorised web access. The information in the database is structured what allows the Yahoda user a more flexible search for required information and at the same time Yahoda provides some basic taxonomy.
In the paper we describe how the database is organised, what are the main features, what information is currently available, how the repository is maintained. We also give a brief summary of future plans and possible developments. As a demonstration we would like to use the data of the Tools Day accepted tools.