The parallel implementation of the Astr\'{e}e static analyzer

TL;DR

This paper discusses the development of a parallel implementation of the Astrée static analyzer, aimed at improving analysis efficiency for large critical programs while maintaining accuracy.

Contribution

It introduces a parallel version of Astrée, enhancing analysis speed without compromising the tool's ability to prove absence of runtime errors.

Findings

Parallel implementation reduces analysis time significantly.

Maintains accuracy in error detection.

Suitable for industrial-scale programs.

Abstract

The Astr\'{e}e static analyzer is a specialized tool that can prove the absence of runtime errors, including arithmetic overflows, in large critical programs. Keeping analysis times reasonable for industrial use is one of the design objectives. In this paper, we discuss the parallel implementation of the analysis.