E0 227 Program Analysis and Verification
Instructors:
Deepak D'Souza,
Aditya Nori,
and Sriram
Rajamani.
Program verification has become an exciting discipline that combines
theory and practice. From a theoretical perspective, the meaning of a
computer program, and automatically proving programs correct have been
the subject of deep investigation in several subdisciplines of
computer science, and they have given rise to several approaches such
as program analysis, theorem proving, model checking and abstract
interpretation.
From a practical perspective, commercial software development
companies are beginning to use various kinds of program verifiers
(and bug finders) in their daytoday development processes.
We will assume that students have exposure to programming, and some
basic knowledge in logic, automata theory, and formal languages.
However, no prior knowledge of program verification or analyses is
assumed.
This course will introduce entering graduate students to the theory and
practice of program analysis. Side by side, we will teach theory, and
through a series of projects, we will build practical program verification
tools (by extending and experimenting with publicly available
verification tools).
 Course outline
 Overview and State of the art (Sriram).

Overview of the course,
and quick tour of representative static analysis tools: ASTREE,
FindBugs, ESPx/SAL,Saturn,SLAM, BLAST, Spec\#, CQual.
 Simple analysis: FindBugs [findbugs05]
 Abstract interpretation: ASTREE [astree03].
 Bytecode verification [leroy01].
 SAL and ESPx [espx06]
 Cqual [cqual_toplas].
 SLAM and Static Driver Verifier [sdv06].
 Spec# and Boogie [specsharp04,boogie05].
 Saturn.
 BDDBDDB [whaley05]
 Type Checking and Type State Verification (Sriram):
 Standard type checking and type inference
 Specifying type systems using datalog
 Nonstandard Type inference  using types to do verification,
Type state checking (Vault [vault] and CQual [cqual_toplas]),
Effective type state verification in the presence of aliasing
[ibm_typestate06]
 Typebased pointer analyses [das00,antgrass07,sridharan06]
 Dataflow analysis (Deepak):
 global program optimization [kildall73]
 Contextsensitive analyses: Time and tape complexity of
pushdown automata languages [ahu68], Dyke reachability
(reachability in graphs) [cfl_reach95], Set constraints (fixpoint
of constraint system) [kodumal04], BDDBDDB [whaley05].
 Hardness results [landi91], [muth00], [chaka03]
 Assertional reasoning (Aditya):
 An axiomatic basis for computer programming [hoarecacm69],
Symbolic execution and program testing [king76].
 An interpretation oriented theorem prover over integers
[kingfloyd70], Simplify [simplify05]
 Practice: ESC, Spec\#/Boogie, George Necula's PCC system
(using the Simplify prover)
 Model checking (Aditya):
 Push down model checking
 Abstraction refinement
 SLAM, BLAST and MOPS (Hao Chen's tool)
 Abstract interpretation (Deepak):
 Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints [cc77],
Systematic design of program analysis frameworks [cc79];
 Abstract domains: Boolean logic [bryant92],linear arithmetic
(difference logic [dbm01],polyhedra [halbwachs78]), uninterpreted
functions [combine06], Combination of LA and UIF [combine06],
arrays

Books and other material

Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of
Program Analysis, Springer, 1999.
 Benjamin Pierce: Foundational
Calculi for Programming Languages, CRC Handbook of
Computer Sc and Engineering, 1995.
 [saturn07]
Alex Aiken, Suhabe Bugrara, Isil Dillig, Thomas Dillig, Brian Hackett, and
Peter Hawkins.
\newblock An overview of the saturn project.
\newblock In PASTE, pages 4348, 2007.
 [ahu68]
Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman.
\newblock A recognition algorithm for pushdown store systems.
In Proceedings of the 1968 23rd ACM national conference, pages
597604, New York, NY, USA, 1968. ACM Press.
 [sdv06]
Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con
McGarvey, Bohus Ondrusek, Sriram K. Rajamani, and Abdullah Ustuner.
Thorough static analysis of device drivers.
In EuroSys '06: Proceedings of the 2006 EuroSys conference,
pages 7385, New York, NY, USA, 2006. ACM Press.
 [astree03]
Bruno Blanchet, Patrick Cousot, Radhia Cousot, J\'{e}rome Feret, Laurent
Mauborgne, Antoine Min\'{e}, David Monniaux, and Xavier Rival.
A static analyzer for large safetycritical software.
In PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on
Programming language design and implementation, pages 196207, New York,
NY, USA, 2003. ACM Press.
 [boogie05]
Michael Barnett, BorYuh Evan Chang, Robert DeLine, Bart Jacobs, and
K. Rustan M. Leino.
Boogie: A modular reusable verifier for objectoriented programs.
In FMCO, volume 4111 of Lecture Notes in Computer
Science, pages 364387, 2005.
 [specsharp04]
Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte.
The spec\# programming system: An overview.
In CASSIS, volume 3362 of Lecture Notes in Computer
Science, pages 4969, 2005.
 [bryant92]
Randal E. Bryant.
Symbolic boolean manipulation with ordered binarydecision diagrams.
ACM Comput. Surv., 24(3):293318, 1992.
 [cc77]
Patrick Cousot and Radhia Cousot.
Abstract interpretation: a unified lattice model for static analysis
of programs by construction or approximation of fixpoints.
In POPL '77: Proceedings of the 4th ACM SIGACTSIGPLAN symposium
on Principles of programming languages, pages 238252, New York, NY, USA,
1977. ACM Press.
 [cc79]
Patrick Cousot and Radhia Cousot.
Systematic design of program analysis frameworks.
In POPL '79: Proceedings of the 6th ACM SIGACTSIGPLAN symposium
on Principles of programming languages, pages 269282, New York, NY, USA,
1979. ACM Press.
 [halbwachs78]
Patrick Cousot and Nicolas Halbwachs.
Automatic discovery of linear restraints among variables of a
program.
In POPL, pages 8496, 1978.
 [chaka03]
Venkatesan T. Chakaravarthy.
New results on the computability and complexity of pointsto
analysis.
In POPL '03: Proceedings of the 30th ACM SIGPLANSIGACT
symposium on Principles of programming languages, pages 115125, New York,
NY, USA, 2003. ACM Press.
 [das00]
Manuvir Das.
Unificationbased pointer analysis with directional assignments.
In PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on
Programming language design and implementation, pages 3546, New York, NY,
USA, 2000. ACM Press.
 [vault]
Robert DeLine and Manuel Fahndrich.
Enforcing highlevel protocols in lowlevel software.
In PLDI, pages 5969, 2001.
 [simplify05]
David Detlefs, Greg Nelson, and James B. Saxe.
Simplify: a theorem prover for program checking.
J. ACM, 52(3):365473, 2005.
 [cqual_toplas]
Jeffrey S. Foster, Robert Johnson, John Kodumal, and Alex Aiken.
Flowinsensitive type qualifiers.
ACM Trans. Program. Lang. Syst., 28(6):10351087, 2006.
 [ibm_typestate06]
Stephen Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay.
Effective typestate verification in the presence of aliasing.
In ISSTA '06: Proceedings of the 2006 international symposium on
Software testing and analysis, pages 133144, New York, NY, USA, 2006. ACM
Press.
 [combine06]
Sumit Gulwani and Ashish Tiwari.
Combining abstract interpreters.
In PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on
Programming language design and implementation, pages 376386, New York,
NY, USA, 2006. ACM Press.
 [espx06]
Brian Hackett, Manuvir Das, Daniel Wang, and Zhe Yang.
Modular checking for buffer overflows in the large.
In ICSE '06: Proceeding of the 28th international conference on
Software engineering, pages 232241, New York, NY, USA, 2006. ACM Press.
 [antgrass07]
Ben Hardekopf and Calvin Lin.
The ant and the grasshopper: fast and accurate pointer analysis for
millions of lines of code.
In PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on
Programming language design and implementation, pages 290299, New York,
NY, USA, 2007. ACM Press.
 [hoarecacm69]
C. A. R. Hoare.
An axiomatic basis for computer programming.
Commun. ACM, 12(10):576580, 1969.
 [findbugs05]
David Hovemeyer, Jaime Spacco, and William Pugh.
Evaluating and tuning a static analysis to find null pointer bugs.
In PASTE '05: Proceedings of the 6th ACM SIGPLANSIGSOFT
workshop on Program analysis for software tools and engineering, pages
1319, New York, NY, USA, 2005. ACM Press.
 [kodumal04]
John Kodumal and Alex Aiken.
The set constraint/cfl reachability connection in practice.
In PLDI '04: Proceedings of the ACM SIGPLAN 2004 conference on
Programming language design and implementation, pages 207218, New York,
NY, USA, 2004. ACM Press.
 [kingfloyd70]
James C. King and Robert W. Floyd.
An interpretation oriented theorem prover over integers.
In STOC '70: Proceedings of the second annual ACM symposium on
Theory of computing, pages 169179, New York, NY, USA, 1970. ACM Press.
 [kildall73]
Gary A. Kildall.
A unified approach to global program
optimization.
In POPL '73: Proceedings of the 1st annual ACM SIGACTSIGPLAN
symposium on Principles of programming languages, pages 194206, New York,
NY, USA, 1973. ACM Press.
 [king76]
James C. King.
Symbolic execution and program testing.
Commun. ACM, 19(7):385394, 1976.
 [leroy01]
Xavier Leroy.
Java bytecode verification: An overview.
In CAV, volume 2102 of Lecture Notes in Computer Science,
pages 265285, 2001.
 [landi91]
William Landi and Barbara G. Ryder.
Pointerinduced aliasing: a problem taxonomy.
In POPL '91: Proceedings of the 18th ACM SIGPLANSIGACT
symposium on Principles of programming languages, pages 93103, New York,
NY, USA, 1991. ACM Press.
 [whaley05]
Monica S. Lam, John Whaley, V. Benjamin Livshits, Michael C. Martin, Dzintars
Avots, Michael Carbin, and Christopher Unkel.
Contextsensitive program analysis as database queries.
In PODS '05: Proceedings of the twentyfourth ACM
SIGMODSIGACTSIGART symposium on Principles of database systems, pages
112, New York, NY, USA, 2005. ACM Press.
 [muth00]
Robert Muth and Saumya Debray.
On the complexity of flowsensitive dataflow analyses.
In POPL '00: Proceedings of the 27th ACM SIGPLANSIGACT
symposium on Principles of programming languages, pages 6780, New York,
NY, USA, 2000. ACM Press.
 [dbm01]
Antoine Min{\'e}.
A new numerical abstract domain based on differencebound matrices.
In PADO, pages 155172, 2001.
 [cfl_reach95]
Thomas Reps, Susan Horwitz, and Mooly Sagiv.
Precise interprocedural dataflow analysis via graph reachability.
In POPL '95: Proceedings of the 22nd ACM SIGPLANSIGACT
symposium on Principles of programming languages, pages 4961, New York,
NY, USA, 1995. ACM Press.
 [sridharan06]
Manu Sridharan and Rastislav Bod\'{\i}k.
Refinementbased contextsensitive pointsto analysis for java.
In PLDI, pages 387400, 2006.
 [Tarski55] Alfred Tarski:
A latticetheoretic fixpoint
theorem and its applications, Pacific J. Mathematics, 5, pages
285309, 1955.
 Lecture slides:
 Overview Lecture 1, zipped version.
 Overview of tools
 Typing
 Data Flow Analysis
 AssertionBased Reasoning
 Abstract Interpretation
Lectures 23&24.
 Model Checking
 Logical Abstract Interpretation (Sumit Gulwani)
 Lecture notes (scribed by Arnab De and K R
Raghavendra) last updated on 26 Sept 2007.
 Assignments

Weightage for evaluation:

Assignments (Lab + written) + Seminar: 60%

Final Exam: 40%

Current meeting schedule: Mon, Wed 10:00am, in EClassroom,
CSA Dept. Tutorial/Seminar slot: Thu 10:00am in EClassroom.

Weightage for evaluation:

Assignments (Lab + written) + Seminar: 60%

Final Exam: 40%

Current meeting schedule: Mon, Wed 10:00am, in EClassroom,
CSA Dept. Tutorial/Seminar slot: Thu 10:00am in EClassroom.
 Exam Schedule:

Final Exam: 10:00am Wed 5th December 2007.