NYU, Graduate Division, Computer Science Course, G22.3033-011 

 Program Semantics, Analysis, and Verification by Abstract Interpretation 

 Patrick Cousot 
pcousot[at]cs[dot]nyu[dot]edu

 Spring 2009 

Course Description:

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).

Recommended Prerequisites:

A basic understanding of logic, sets, proofs, recursion, languages, grammars and attribute is recommended, these prerequisites are covered in class 1.

Schedule:

Wednesday, 5:00—6:50, CIWW 202 Office Hours: By email appointment on Wednesday, 3:00—4:30, CIWW 405

Textbooks:

Course notes provided by the instructor.

Course requirements:

Homeworks (exercices).

First course:

January 21st, 2008.

Grading:

Homeworks (20%), mid-term exam (40%), and final exam (40%).

Course content:

Available at G22.3033-011, spring 09, program semantics, analysis, and verification by abstract interpretation