Static Analysis of Communicating Processes using Symbolic Transducers
This addresses verification challenges for concurrent systems like those using MPI, though it appears incremental as it builds on Regular Model Checking and abstract interpretation frameworks.
The researchers tackled the problem of verifying safety properties in systems of communicating processes by developing a static analysis technique using symbolic transducers and abstract interpretation, which they implemented in a prototype targeting MPI C programs to soundly over-approximate reachable states.
We present a general model allowing static analysis based on abstract interpretation for systems of communicating processes. Our technique, inspired by Regular Model Checking, represents set of program states as lattice automata and programs semantics as symbolic transducers. This model can express dynamic creation/destruction of processes and communications. Using the abstract interpretation framework, we are able to provide a sound over-approximation of the reachability set of the system thus allowing us to prove safety properties. We implemented this method in a prototype that targets the MPI library for C programs.