TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 00481

Logic, Algebra, and Formal Verification of Concurrent Systems

( Nov 26 – Dec 01, 2000 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/00481

Organizers
  • A. Muscholl (Paris)
  • D. A. Peled (Bell Labs, Murray Hill)
  • M. Droste (Dresden)
  • V. Diekert (Stuttgart)



Motivation

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.

Participants
  • A. Muscholl (Paris)
  • D. A. Peled (Bell Labs, Murray Hill)
  • M. Droste (Dresden)
  • V. Diekert (Stuttgart)