Proving the absence of errors in software is usually not a big concern. “What if my program crashes? Whatever, I will just restart it.” But sometimes, a program that crashes is a big issue: it may cause deaths, cost a lot of money or compromise privacy. Such software is called critical, and it is interesting to prove some properties like the absence of run-time errors (like divisions by 0), that the result is what we expect or that the program terminates quickly enough.
Abstract interpretation is a general method allowing to prove such properties using approximation of semantics. The most classical example is the rule of signs for multiplication: whatever the value of two numbers, if they have the same sign, the result is non-negative. From a partial knowledge on the prior state, we deduce some facts on the result. Hopefully, we deduce a fact that is sufficient to prove our interest property.
In general, properties we are interested in (like the absence of errors) are not computable: as a consequence of Rice’s theorem, there is no algorithm that determines if any program is error-free. To find all possible bugs automatically, we must accept to detect bugs that exist only in the approximate semantics. The point of abstract interpretation is to build approximation precise enough to prove what we want, but coarse enough to be scale up to real life applications.
This talks is an example-driven introduction to abstract interpretation.