Keynote Speech III

As network and multi-core systems are becoming pervasive, software systems also go concurrent. In a concurrent setting, in order to accomplish its computation task a program must cooperate with other programs by exchanging messages between them. These result in non-determinism and sophisticated interaction behavior, making it very difficult to ensure that concurrent software systems will run safely and reliably In this talk I will present an approach to checking safety properties of concurrent programs. In this approach, concurrent programs are represented as symbolic transition graphs which can be regarded as a generalization of flow chart diagrams to allow nondeterminism and communication. Safety properties are expressed as formulas in alteration-free first-order mu-calculus. An efficient algorithm exists to check whether a symbolic transition graph satisfies the desired properties. Various abstraction techniques can be incorporated to reduce the size of reachable state space.