Deciding the Undecidable

A fundamental intellectual achievement in Computer Science, dating back to the 1930s, is the observation that that there is a universal notion of computability and that some problems are actually uncomputable. This is not merely a philosophical curiosity, but a concrete problem for the design and implementation of programming languages, since it turns out that every interesting question about the behavior of programs is undecidable in the sense of its answers being uncomputable. This includes questions about the correctness of programs, their running times, their resource consumptions, and the applicability of most optimizations. Fortunately, for practical purposes it is often sufficient to obtain conservative and approximate answers to these questions. The efficient computation of useful answers is the challenge that has given rise to the research area of static program analysis, which has an established mathematical basis but also a strong engineering flavor for real-life languages and questions. We present the foundations of static analysis and give examples of recent projects that use these techniques to combat undecidability.