Formal Methods Wiki

Virtual Library
Software engineering
Formal methods

Please add information and links relevant to concurrent systems to this page. Alternatively, please contact Jonathan Bowen if you know of relevant online information not included here or would like to maintain information on a particular topic.

This document contains some pointers to information on concurrent systems available around the world on the World Wide Web (WWW).

! indicates new entries. * indicates a (subjectively!) recommended link for especially good online information.

Electronic repositories[]

If you are searching for on-line Technical Reports, you may find the Unified Computer Science Technical Report Index helpful. E.g., see a list of Technical Reports concerned with concurrency, concurrent, parallel and distributed systems. See also a list of Computer Science Technical Reports archive sites.

Research groups and centers[]

Tools, process algebras, etc.[]

Concurrency tools:

  • CADP, a widespread toolbox for the Construction and Analysis of Distributed Processes.
  • CWB (Edinburgh Concurrency Workbench) automated toolset. See also the Concurrency Factory and CWB-NC (The Concurrency Workbench of North Carolina), which includes a LOTOS interface, diagnostic infomation, etc. Note: The CWB and CWB-NC have a common ancestor, but are each under separate development.
  • Concurrency Factory, a "next generation" Concurrency Workbench toolkit.
  • Circal (CIRcuit CALculus) System supporting a process algebra which may be used to rigorously describe, verify and simulate concurrent systems. See software.
  • DI2PN tool. Delay Insensitive circuits and Petri Nets.
  • FDR2 (Failures-Divergence Refinement) for CSP.
  • LTSA (Labelled Transition System Analyser), a verification tool for concurrent systems. See also associated Concurrency: State Models & Java Programs book by Jeff Magee and Jeff Kramer (published by Wiley, 1999).
  • Meije tools for the verification of concurrent programs. It contains: ATG, an X-based editor for labelled automata and networks of synchronized automata; Mauto, a tool for computing transition systems from programs in CCS, Basic Lotos, Meije, or Esterel, reducing them along various bisimulations; Hoggar, a batch tool for fast reduction (for strong, weak, and branching bisimulations) of systems described in FC2 format, using either BDDs or explicit representations.
  • TAPAs (Tool for the Analysis of Process Algebras): TAPAs aim is to support teaching of process algebras. It can be use to specify and analyze concurrent systems. Systems are described as process algebras terms that are then mapped to Labelled Transition Systems (LTSs). Properties can be verified by checking equivalences between concrete and abstract system descriptions, or by model checking temporal formulas over the obtained LTS. A key feature of TAPAs, that makes it particularly suited for teaching, is that it maintains a consistent double representation of each system: both graphical and textual.
  • VERSA — Verification Execution and Rewrite System for ACSR.

Process algebras:

Development methods:

Three disciplines for the design of asynchronous circuits</A>, from the Centre for Concurrent Systems and VLSI. Real-time and reactive systems:

Research projects[]


Last updated by Jonathan Bowen, 16 March 2009.
Further information for possible inclusion is welcome.