• People
• Events
• Research

Analysing Mutual Exclusion Algorithms Using CCS

Abstract: A number of algorithms intended to ensure mutually exclusive execution of certain `critical sections' of code are studied by representing them as CCS agents and employing an automated tool, the Concurrency Workbench, to analyse the representations. The problem of determining whether or not each of the algorithms does indeed preserve mutual exclusion is considered.

LFCS report ECS-LFCS-88-45

This report was published in Formal Aspects of Computing, 1(3): 273--292, 1989.