Modular static analysis for soft contract verification of distributed actor programs

Distributed programs, where multiple independent systems
communicate and coordinate with each other in order to reach a
common goal, have become more ubiquitous over the years. Actor
programming presents an apt model for describing and implementing
such distributed systems. Unfortunately, programmers tend to make
more mistakes and introduce more bugs in distributed programs than
sequential ones, due to the fact that challenging factors in distributed
programs such as partial failures are often underestimated. Designby-contract programming has proven to be a powerful paradigm to
specify the intended behaviour of a program, and therefore making it
more robust. Unfortunately, the enforcement of these contracts
usually introduces a large run-time overhead.
We propose to develop a novel contract language for distributed
actor programs. To minimize run-time overhead and to detect
potential defects ahead of time, we aim to bring soft contract
verification to distributed programs in order to statically verify as
many contract checks as possible, leaving the unverified ones as
residuals to be checked at run time. Distributed programs are
challenging to statically analyse, due to non-determinism introduced
by message multiplicity and partial failures. We will approach softcontract verification through a process-modular analysis, while
striking an appropriate balance between analysis precision and
scalability.