Programmers revel in specifications, descriptions, and abstractions. _Abstract interpretation_ is the formal theory of what an abstraction is and how an abstraction reveals aspects of the real-world object that it describes. But the theory also shows us that ``real-world objects'' are themselves abstractions (of other real-world objects) such that, ultimately, everything is an abstraction of something else.
We will survey the basics of abstract interpretation and apply them to a range of computing examples, such as data-typing systems, operational semantics definitions, program proving, and code improvement. Finally, we will see how abstract-intepretation techniques let us understand that the currently popular technique of ``model checking'' finite-state systems is just a typical instance of an abstract interpretation.