Abstract interpretation is a technique which has allowed the development of very powerful program analyzers and transformers, which are at the same time provably correct and highly practical. We will first present the basics of abstract interpretation and of parametric abstract interpretation frameworks (i.e., those in which different abstract domains –analyses– are “plug-ins”). We will then explore the components of an abstract interpretation-based framework for validating programs with respect to partial specifications written using assertions, detecting and locating bugs, simplifying run-time tests, performing high-level program transformations, and enriching mobile code with certificates.