CIS 890, Program Analysis and Computability, Fall 2010

Instructor:

Torben Amtoft

Time:

Tuesdays, 9:30-11:30am in N236.

Form of class:

Presentations by students and instructor, leading to class discussions. (Larger projects could arise from this class.)

Log

August 24

Introduction to course.

• We introduce ourselves
• Torben motivates program analysis
• Torben outlines basic concepts in lattice theory

August 31

Joseph leads us through the first 4 sections of Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints by Patrick Cousot and Radhia Cousot.

September 7

Joseph finishes the Cousot-paper; we work out several examples that help us understand the paper better.

September 14

Vineet presents Chapter 1 of Principles of Program Analysis by Nielson & Nielson & Hankin, giving a brief introduction to

• Data Flow Analysis (which is either "may" or "must", and either "forward" or "backward")
• Control Flow Analysis
• Abstract Interpretation

September 21

Jason presents Volpano & Smith & Irvine's A Sound Type System for Secure Flow Analysis. We also discuss some limitations of non-interference, like if

• termination is observable
• computation time is observable
• secrets are partially leaked

September 28

Balaji introduces Turing machines, including

• apparent extensions, such as multi-tape and non-determinism
• apparent restrictions, such as two-stack machines and counter machines

Torben then outlines the principle of diagonalization, for instance used to show that the real numbers are not countable.

October 5

• Balaji presents a diagonalization argument that shows that it is undecidable if a Turing machine is "circle-free".
• Torben summarizes the results of Kurt Goedel, in particular his completeness theorem (a sentence that is true in all models can be proved) and his incompleteness theorem (there are sentences that are true for the standard model of natural numbers but cannot be proved).

October 12

Torben introduces the concepts of NP, and NP-hardness.

October 19

• Vineet finishes his September 14th presentation by presenting various kinds of type systems.
• Torben presents a lot of other NP-hard problems, with corresponding reductions from SAT.

October 26

• Jason presents a detailed proof that SAT is NP-hard.
• Balaji presents Section 11.1 (on co-NP), and the beginning of 11.2 (on PSPACE), in Introduction to Automata Theory, Languages, and Computation by Hopcroft & Motwani & Ullman (3rd edition).

November 2

• Torben presents some basic results on the feasibility of approximation algorithms.
• Jason presents Section 11.4 in the Hopcroft et al textbook, on randomization-based language classes.

November 9

• Joseph argues that 2SAT is in P.
• Balaji covers Section 11.2, on PSPACE, and Section 11.5, on primality testing, in the Hopcroft et al textbook.

November 16

First some brief presentations:

• Vineet gives an algorithm to find a satisfying truth assignment for a 2SAT problem.
• Balaji finishes Section 11.5 in the Hopcroft et al textbook, in particular shows that primality testing is in NP.

Then Joseph prepares for non-standard analysis by introducing (ultra)filters.

November 30

Last day of class.

• Vineet outlines his recent work on constructing evidence for information flow analysis.
• Torben sketches how to construct (in polynomial time) a satisfying assignment for a 2SAT problem.
• Joseph introduces the key concepts behind non-standard analysis, and illustrates by examples.