CS 798G: Analysis of Unconventional Programs

Credits: 3-0-0-0 (9)

 

Prerequisites

The course will expect the students to have a good understanding of the theory of computations (especially computation models, languages, decidability etc.), algorithms (especially complexity analysis, correctness proofs), Discrete Mathematics (especially proof techniques, linear algebra, lattice theory, fixpoint theory), Probability and Statistics. The course will include challenging programming assignments and projects, so the students will be expected to be good programmers.

 

Objective

Over the last few years, program analysis techniques have been applied to a variety of systems. Many of these cannot be perceived as “conventional” sequential programs written in languages like C, Python or Java. For example, there have been attempts at testing and verifying network routing policies, machine language models, database schemas, concurrent systems, probabilistic/randomized systems and hardware/software co-designs. This course will explore how program analysis techniques have been adapted for such “unconventional” programs.

 

Syllabus

1. Programming Language Fundamentals: syntax and semantics, type systems;
2. Program Analysis of Sequential Programs: control-flow and dataflow analysis, abstract interpretation, deductive verification, fuzzing, symbolic execution;
3. Analysis of concurrent systems: memory consistency models, duductive techniques (like Owicki-Gries), vector-clock based dynamic techniques;
4. Analysis of probabilistic and reandomised systems: syntax and semantics of probabilistic operations, modeling probabilistic distributions, applications (eg. differential privacy, randomized algorithms etc.);
5. Analysis of machine learning systems: relevant properties (robustness, fainess, safety etc.) in the context of ML systems, testing/analysis of ML models;
6. Parallels between program analysis and analysis of hardware designs/co-designs;
7. Analysis of miscellaneous other systems, like quantum programs, network control planes and database schemas.

 

Resources

There is no textbook for the course. The course will be based on relevant research papers.