The aim of the paper is to share the design problems we experienced when we were implementing a prototype analyzer of an asynchronous concurrent language. This new kind of static analyzer is based on previous work about operational semantics of parallel languages that can express concurrency and non-determinism of actions: it constructs abstract automata reflecting all the possible execution behaviours of programs written in languages such as Parallel Pascal [Cri95] or Concurrent ML [Cri96].
We will also present some experimental results dealing with the size of the generated automata and the precision of the analysis. For instance some well-known mutual exclusion protocols have been automatically proven correct. The analyzer has been interfaced using the HTML markup language: this allows the user to ask for computed invariants at given program points.