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