Modular static analysis for soft contract verification of distributed actor programs

Project Details

Description

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.
AcronymFWOTM1089
StatusActive
Effective start/end date1/11/2131/10/25

Keywords

  • distributed program verification
  • design-by-contract
  • static analysis

Flemish discipline codes 2018-2023

  • Computer science

Fingerprint

Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.
  • Cross-Level Debugging for Static Analysers

    Van Molle, M., Vandenbogaerde, B. & De Roover, C., 23 Oct 2023, Proceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering (SLE ’23): SPLASH 2023. Saraiva, J., Degueule, T. & Scott, E. (eds.). New York, NY, USA: ACM, p. 138-148 11 p. (SLE 2023 - Proceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering, Co-located with: SPLASH 2023).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

    Open Access
    File
    8 Downloads (Pure)
  • Summary-Based Compositional Analysis for Soft Contract Verification

    Vandenbogaerde, B., Stiévenart, Q. & De Roover, C., 2022, Proceedings - 2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation, SCAM 2022: 2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation (SCAM). 22 ed. IEEE, p. 186-196 11 p. (Proceedings - 2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation, SCAM 2022).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

    Open Access
    File
    1 Citation (Scopus)
    17 Downloads (Pure)