Anonymous On-line Communication Between Program Analyses

TL;DR

This paper introduces a lightweight, anonymous, on-line communication model for different program analyses, enhancing their effectiveness without significant modifications, demonstrated through a case study with three analyses.

Contribution

It presents a novel anonymous communication protocol enabling independent program analyses to collaborate online without compromising their implementations.

Findings

Improvements in computed invariants

Increased number of successfully analyzed benchmarks

Effective collaboration among diverse analyses

Abstract

We propose a light-weight client-server model of communication between existing implementations of different program analyses. The communication is on-line and anonymous which means that all analyses simultaneously analyse the same program and an analysis does not know what other analyses participate in the communication. The anonymity and model's strong emphasis on independence of analyses allow to preserve almost everything in existing implementations. An analysis only has to add an implementation of a proposed communication protocol, determine places in its code where information from others would help, and then check whether there is no communication scenario, which would corrupt its result. We demonstrate functionality and effectiveness of the proposed communication model in a detailed case study with three analyses: two abstract interpreters and the classic symbolic execution. Results of the evaluation on SV-COMP benchmarks show impressive improvements in computed invariants and increased counts of successfully analysed benchmarks.