Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers

TL;DR

This paper discusses the challenges, solutions, and trade-offs in designing formally verified static analysis tools, especially for verified compilers, balancing correctness and efficiency in implementation.

Contribution

It provides insights into the design choices and trade-offs involved in creating formally verified static analyzers that are both correct and practically efficient.

Findings

Identifies key difficulties in verified static analysis.

Proposes possible solutions and design strategies.

Highlights trade-offs between correctness and efficiency.

Abstract

Formally verified compilers and formally verified static analyzers are a solution to the problem that certain industries face when they have to demonstrate to authorities that the object code they run truly corresponds to its source code and that it satisfies certain properties. From a scientific and technological point of view, they are a challenge: not only a number of nontrivial invariants and algorithms must be proved to be correct, but also the implementation must be reasonably effective so that the tools operate within reasonable time. Many optimizations in compilers rely on static analysis, and thus a formally verified compiler entails formally verified static analyses.In this article, we explain some difficulties, possible solutions, design choices and trade-offs pertaining to verified static analysis, in particular when the solution of the analysis is expressed as some form of tree, map or set.