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.
Abstract Interpretation is a theory of approximation of mathematical structures, in particular those involved in the semantic models of computer systems. Abstract interpretation can 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 semantics (the formal description of actual program executions), specifications (the formal description of the expected behaviors of programs), verification (the mathematical proof that program executions conform to their specification), and static analysis (the automatic, compile-time determination of run-time properties of programs).