Summary-Based Compositional Analysis for Soft Contract Verification

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

1 Citation (Scopus)
35 Downloads (Pure)

Abstract

Design-by-contract is a development best practice
that requires the interactions between software components to
be governed by precise specifications, called contracts. Contracts
often take the form of pre- and post-conditions on function
definitions, and are usually translated to (frequently redundant)
run-time checks. So-called soft contract verifiers have been
proposed to reduce the run-time overhead introduced by such
contract checks by verifying parts of the contracts ahead of
time, while leaving those that cannot be verified as residual runtime checks. In the state of the art, static analyses based on
the Abstracting Abstract Machines (AAM) approach to abstract
interpretation have been proposed for implementing such soft
verifiers. However, these approaches result in whole-program
analyses which are difficult to scale.
In this paper, we propose a scalable summary-based compositional analysis for soft contract verification, which summarises
both the correct behaviour and erroneous behaviour of all
functions in the program using symbolic path conditions. Information from these summaries propagates backwards through
the call graph, reducing the amount of redundant analysis
states and improving the overall performance of the analysis.
This backwards flow enables path constraints associated with
erroneous program states to flow to call sites where they can be
refuted, whereas in the state of the art they can only be refuted
using the information available at the original location of the
error.
To demonstrate our improvements in both precision and performance compared to the state-of-the-art, we implemented our
analysis in a framework called MAF (short for Modular Analysis
Framework) — a framework for the analysis of higher-order
dynamic programming languages. We conducted an empirical
study and found an average performance improvement of 21%,
and an average precision improvement of 38.15%.
Original languageEnglish
Title of host publicationProceedings - 2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation, SCAM 2022
Subtitle of host publication2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation (SCAM)
PublisherIEEE
ChapterStatic Analysis
Pages186-196
Number of pages11
Edition22
ISBN (Electronic)978-1-6654-9609-4
DOIs
Publication statusPublished - 2022
Event2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation (SCAM) - Limassol, Cyprus
Duration: 3 Oct 20224 Oct 2022
Conference number: 22

Publication series

NameProceedings - 2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation, SCAM 2022

Conference

Conference2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation (SCAM)
Abbreviated titleSCAM 2022
Country/TerritoryCyprus
CityLimassol
Period3/10/224/10/22

Bibliographical note

Funding Information:
Partially funded by Research Foundation Flanders (FWO) (grant number 1187122N).

Publisher Copyright:
© 2022 IEEE.

Keywords

  • abstract interpretation
  • design-by-contract
  • soft contract verification
  • static analysis

Fingerprint

Dive into the research topics of 'Summary-Based Compositional Analysis for Soft Contract Verification'. Together they form a unique fingerprint.

Cite this