We trace the roots of abstract interpretation and its role as a fundamental theoretical framework to understand and design program analysis and program verification methods. Starting from the historical roots of program verification and formal methods, from A.M. Turing to C.A.R. Hoare, we show how abstract interpretation fits this mainstream in perfect continuity and how this theory shaped the literature and the practice in program analysis in the last 40 years, providing powerful methodologies for designing static program analyzers, automatic verifiers of software/hardware systems, type systems, security protocol analyzers, analyzers of machine learning models, algorithms for formal languages.
展开▼
