Abstract

Static analysis is an approach to determine information about the program without actually executing it. There has been much research in the static analysis of concurrent programs. However, very little academic research has been done on the formal analysis of message passing or process-oriented languages. We currently miss formal analysis tools and techniques for concurrent process-oriented languages such as Erasmus . In this dissertation, we focus on the problem of static analysis of large Erasmus programs. This can help us toward building more reliable Erasmus software systems.
Reasoning about non-deterministic large Erasmus program using static analyzer is hard. These kinds of programs can quickly exhaust the computational and memory resources of the static analyzer tool. We use Abstract Interpretation to reason about Erasmus programs.
To use the Abstract Interpretation theory, we introduce a lattice for Erasmus communications and an Event Order Predictor algorithm to statically determine the order that events happen in an Erasmus program. By using fixed-point theory of lattice, we compute a safe approximation of reachable states of an Erasmus programs. We also offer a Resettable Event order Vector for Erasmus processes to realistically implement our vector for large Erasmus programs using bounded space. We believe that our formal approach is also applicable to other types of process-oriented programs and MPI programs.