CIS 890, Program Analysis and Computability, Fall 2010

Instructor:

Torben Amtoft

Time:

Tuesdays, 9:3011: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 Cousotpaper; 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 noninterference, like if

termination is observable

computation time is observable

secrets are partially leaked

September 28

Balaji introduces Turing machines, including

apparent extensions, such as multitape and nondeterminism

apparent restrictions, such as twostack 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 "circlefree".

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

October 19


Vineet finishes his September 14th presentation
by presenting various kinds of type systems.

Torben presents a lot of other NPhard problems,
with corresponding reductions from SAT.

October 26


November 2


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 nonstandard 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 nonstandard analysis,
and illustrates by examples.
Torben Amtoft