Software-induced memory corruptions can be caused by stack overflows, run-time errors such as invalid pointer accesses or buffer overflows, and data races. They can trigger software crashes, invalidate separation mechanisms in mixed-criticality software, and are a frequent cause of errors in multi-core applications. In contrast to hardware faults, software-induced memory corruptions are always systematic errors, and hence it is possible to formally prove their absence. Abstract interpretation is a formal method for static program analysis which supports formal soundness proofs (it can be proven that no error is missed) and which scales. This article gives an overview of abstract interpretation and its application to prove the absence of stack overflow, run-time errors, and data races, and reports on practical experience with the tools StackAnalyzer and Astrée.