E0 227 Program Analysis and Verification

August-December 2017, 2.00pm-3.30pm Tue Thu, Room 117

Instructors: K. V. Raghavan, Deepak D'Souza

Teaching assistants: P. Ezudheen (ezudheen@gmail.com), Nikita Chopra (nikita@iisc.ac.in)

Assignments

Lecture slides

Motivation

Program analysis is a collection of techniques for computing approximate information about a program. Program analysis finds several applications: in compilers, in tools that help programmers understand and modify programs, and in tools that help programmers verify that programs satisfies certain properties of interest. As software systems have become larger and more complex there has been a lot of practical interest in using program-analysis based tools to assist with software development. In this course we will learn about techniques to reason about the meaning of and the properties of a program, and the theory behind foundational program-analysis techniques such as abstract interpretation, type systems, and theorem proving. We will also look at an important application of program analysis, namely the operation of program slicing.

We will assume that students have exposure to programming, the fundamental concepts of programming languages, and the basics of mathematical logic and discrete structures. However, no prior knowledge of program analysis is assumed.

Syllabus

Abstract Interpretation: Lattices, abstract join-over-all-paths analysis of a program. Correctness of abstract information: Galois connections, abstract interpretation as an over-approximation of concrete semantics. Dataflow analysis: Computing an over-approximation of join-over-all-paths information using Kildall's algorithm, by modeling the statements in the program as a set of equations. Analysis of multi-procedure programs. Type Systems: Monomorphic type systems. Pointer analysis of imperative programs. Program slicing. Assertional reasoning using Hoare logic.

Reading material