Some Experience on the Software Engineering of Abstract Interpretation Tools

AbstractThe “right” way of writing and structuring compilers is well-known. The situation is a bit less clear for static analysis tools. It seems to us that a static analysis tool is ideally decomposed into three building blocks: (1) a front-end, which parses programs, generates semantic equations, and supervises the analysis process; (2) a fixpoint equation solver, which takes equations and solves them; (3) and an abstract domain, on which equations are interpreted. The expected advantages of such a modular structure is the ability of sharing development efforts between analyzers for different languages, using common solvers and abstract domains. However putting in practice such ideal concepts is not so easy, and some static analyzers merge for instance the blocks (1) and (2).We show how we instantiated these principles with three different static analyzers (addressing resp. imperative sequential programs, imperative concurrent programs, and synchronous dataflow programs), a generic fixpoint solver (Fixpoint), and two different abstract domains. We discussed our experience on the advantages and the limits of this approach compared to related work