The Pragmatics of HDA for Concurrent Program Analysis

In this paper we discuss the relevance of Higher-Dimensional Automata to program analysis. Most of the work on that model for true-concurrency dealt with the nature of the model itself [Pra91b, vG91], the ways one could use it to give semantics to concurrent programming languages [GJ92, Gou93]. In [CG93, Gou95b] a first step was made towards a practical use of the tools provided by the HDA semantics, whereas in [Cri95, Cri96] a prototype analyser was presented for a concurrent Pascal (and for CML). In this paper, we explain the pragmatics of HDA for concurrent program analysis on various levels: definition and presentation of semantics, expressivity, complexity of the computer representation and implementation issues (complexity of deadlock detection in this model, following [FR96], being given as a good test case). We also introduce a new abstract interpretation for finding and verifying schedules of concurrent systems, some ideas of which have been inspired by some work in concurrent..