Modelling Concurrent Systems

Objectives

The Modelling Concurrent Systems Group conducts research into models of concurrent behavior, with applications to programming and specification languages for parallel and distributed computation. Furthermore, we are looking for techniques for verifying concurrent systems. We develop and maintain the verification platform Truth.

Topics in this area are

• logical descriptions of properties using modal logic
• semantic domains for concurrent systems
• programming languages for concurrent systems
• model checking

Members

• Prof. Dr. Indermark
• Prof. Dr. Thomas
• Benedikt Bollig
• Thomas Noll
• Volker Stolz
• Michael Weber
• Former members

Students:

• Markus Schlütter
• Eric Bodden
• René Theisen
• Carsten Kern
• Michael Rohrbach
• Stefan Rieger

Mailing list

The (low volume) mailing list mcs@lists.rwth-aachen.de informs about local meetings and news. You can use the web interface to subscribe to the mailing list or to read past messages.

Activities and Projects

• Talks
• MSC Execute & MSCan
• MSCan
• Truth
• Game based Model Checking
• SLC - The Specification Language Compiler
• Distributed Model Checking

Literature and other information

• A Mirror of the Concurreny Mailing List
• A Collection of Specification and Verification Tools
• An overview of tools for working with Message Sequence Charts (MSCs)
• An overview of tools for verifying SDL specifications

Links to collections about Concurrency and Formal Methods

• Formal Methods
• Education and Formal Methods
• Concurrent Systems

Links to other concurrency groups

• Formal Methods at Bell Laboratories
• Formal Design Techniques Group at SICS