NYU, Graduate Division, Computer Science Course, G22.3033-011
Program Semantics, Analysis, and Verification by Abstract Interpretation
The fast-growing volume and complexity of software embedded in safety, mission, and business-critical systems is driven by demands for increased functionality while being asked to function at unprecedented levels of reliability, safety, security, and scalability. In this context, automatic software analysis and formal verification to prove the absence of errors becomes a cost-effective complement to empirical validation and testing methods to detect the presence of bugs and flaws in computer systems. It is a basic requisite in the curriculum of advanced software engineers and researchers.
Abstract Interpretation is a theory of approximation of mathematical structures, in particular those involved in the semantic models of computer systems. Abstract interpretation has been be applied to the systematic construction of methods and effective algorithms to approximate undecidable or very complex problems in computer science such that the semantics, the proof, the static analysis, the verification, the safety and the security of software or hardware computer systems. In particular, abstract interpretation-based static analysis, which automatically infers dynamic properties of computer systems, has proven to be effective, precise, and scalable, and has been very successful these last years to automatically verify complex properties of real-time, safety critical, embedded systems.
The course is an introduction to abstract interpretation with applications to static analysis (the automatic, compile-time determination of run-time properties of programs) and software verification (conformance to a specification).