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 2011 

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

Course Topics:

Recommended Prerequisites:

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

Schedule:

Thursday, 5:00PM—6:50PM, WWH 317 Office Hours: By email appointment on Thursday, 2:00PM—2:30PM, CIWW 405

Textbooks:

Electronic course notes provided by the instructor.

Course requirements:

Homeworks (exercices).

First course:

The University was closed and all NYU classes, activities, events, offices and operations were cancelled on Thursday, Jan. 27, due to the widespread disruptions caused by the snow storm. The first class will therefore be on Thursday February 3rd, 2011.

Grading:

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

The course content is online