Static analysis with dioids and polynomial ideals

Static analysis aims to verify that programs behave correctly i.e. satisfy safety properties. However, generating properties verified by a program is a difficult problem : Rice’s theorem states that any non-trivial property about the language recognized by a Turing machine is undecidable. In order to avoid this difficulty, static analyses approximate the possible behaviours of the program. Abtract interpretation theory defines a formal framework for approximating programs. This theory, introduced by Cousot & Cousot is based on the mathematical structure of lattices, Galois connections and iterative fixpoints calculus. This framework defines the notion of correct approximation and allows for qualitatively compare approximations. On the contrary, it is not suitable for handling quantitative properties (such as memory usage and execution time).