Modeling and Verifying Concurrent Programs with Finite Chu Spaces

Finite Chu spaces are proposed for the modeling and verification of concurrent programs. In order to model not only typical concurrent behaviors but also modern exception handling and synchronization mechanisms, we design an enriched process algebra of Chu spaces from a practical point of view. To illustrate the power of finite Chu spaces and the process algebra while abstracting away from language-specific details, an imaginary concurrent programming language (ICL) is designed. A denotational semantics of ICL is presented using finite Chu spaces and the enriched process algebra. The valuation functions are fairly straightforward since the carefully designed operators have done much of the job. The enriched process algebra is also used as the specification language for Chu spaces, with which process-algebraic properties can be specified. Verification algorithms are presented with their time complexities discussed.