In recent years a lot of research was devoted to developing efficient verification and validation techniques for concurrent systems. The goal of the seminar is to bring together people that use and develop formal methods tools, with people developing theories that can potentially enhance the capabilities of such tools. The focus is on research areas within algebra and logic that have shown a strong potential for this integration between theory and practice.

The interaction of different approaches and methodologies has resulted in new verification techniques and improved existing ones. For example, automata on infinite words are a simple and basic mathematical model that has been used as the theoretical basis for state-based automatic verification of temporal logic specifications. Other algebraic-oriented approaches (such as CASL a common language for formal specification of functional requirements and modular software design), have proposed solutions for unifying existing specification and methodological frameworks. A recent example of combining theory and practice is the use of message sequence charts (MSCs). A similar notation is used in formal methods for denoting interaction in object oriented systems, including in the unified modeling language (UML). The theoretical study of this standard notation, used by people in industry, resulted in algorithms that are used to detect errors in preliminary design of communication software. The use of algebraic theories resulted also in a deeper understanding of formal specification. For example, some questions concerning the expressiveness of linear temporal logics were solved using the Krohn-Rhodes theorem about the wreath product decomposition of semigroups. Also, the theory of semigroups contributed to recent progress of questions related to the boundedness problem in database theory, which can be formalized within the framework of commuting actions as the finite power problem. Verification tools that are based on algebra, logic and automata theory include Cospan, Murphy, SMV, Spin, Uppal, PVS, and many others. The developers of such tools are constantly looking forward for new ideas that will allow verifying bigger systems in a faster way.

We expect that the seminar will stimulate the interaction between algebra, logic and development of verification tools by addressing topics related to:

• Appropriate logical formalisms for describing properties of concurrent systems. Selecting the right formalism has an influence on the kind of specification we can give for a system, and the complexity of performing automatic verification.
• Methodologies used for improving the efficiency of verification tools. Identifying the algebraic properties which are relevant for the existing techniques is a necessary background for devising new solutions.
• Algebraic specification formalisms. The increasing complexity and diversification of concurrent systems requires specific formal models for the properties we want to verify automatically.