Formal Verification of a C Value Analysis Based on Abstract Interpretation

Abstract

Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone.