Sound static analysis allows one to overapproximate all possible program executions to infer various properties. However, it requires quite some effort to formalize and prove the soundness of program semantics. Most software applications developed nowadays are distributed systems in which different computational entities communicate through synchronous and asynchronous mechanisms. These applications are composed of programs developed in many programming languages and rely on many technologies. Static analysis might be particularly promising in distributed architectures, where exhaustively (or even partially) testing such systems is often prohibitive. However, distributed architectures intrinsically brings some challenges that need to be carefully taken into considerations during the design of the analyzer. In this talk, we present an analysis for the Robot Operating System 2 (ROS 2), a framework designed for building distributed robotic applications. Then, we will discuss how these techniques can be generalized to other architectures, such as microservices.
