Soft Verification for Actor Contract Systems

Design-by-contract is a software engineering practice where programmers annotate program elements with contract specifications that make expectations towards the user and supplier of the program element explicit. This practice has been applied in various contexts such as higher-order programming languages. However, support for contracts in distributed actor programs is limited. Unfortunately, contract specifications need to be checked while executing the program which introduces a substantial overhead. To counter this, soft verification techniques have been proposed to verify (parts of) contract specifications, but have only been applied in the context of sequential programs. The goal of our research is therefore twofold: designing contract languages for distributed actor programs and developing techniques for their soft verification. In this context, we present a work plan and method, and show our preliminary results.