spacer spacer spacer spacer spacer spacer spacer spacer spacer
spacer spacerPublic home pagespacer spacer spacerLocal home pagespacer spacer spacerHow to contact usspacer spacer spacerSearchspacer spacer
spacer spacer spacer spacer spacer spacer spacer spacer spacer



Techniques for static analysis of source code and modern programming paradigms. Analysis techniques: data flow analysis, program dependence graphs, type-based analysis. The meaning of programs: lambda calculus, denotational semantics. Abstraction mechanisms: polymorphic types, operation overloading, inheritance, object-oriented programming and ML-like programming languages.


Class material

Sept 3 Introduction to O'Caml O'Caml web page
Sept 5 Introduction to Types, and practical subtyping Luca Cardelli, Type Systems, Section 1
Sept 10 ML Modules, First order type systems
  • Luca Cardelli, Type Systems, Sections 2-3
  • Martin, R. C. (1996, Mar). The Liskov Substitution Principle. C++ Report
  • Sept 12 Lambda calculus, higher order type systems
  • Luca Cardelli, Type Systems, Sections 4-6
  • Sept 17 Guest lecture by Jeff Foster
  • A Theory of Type Qualifiers
  • Detecting Format-String Vulnerabilities with Type Qualifiers
  • Sept 19
  • Why Functional Programming Matters
  • Sept 24 Dataflow analysis, use-def chains, etc.
  • A unified approach to global program optimization
  • Oct 1 Abstract Interpretation
    Oct 3 Dominators
  • Abstract Interpretation
  • Oct 8 Reaching Defs and SSA form
    Oct 10
  • "Is it a Tree, a DAG, or a Cyclic Graph? A Shape Analysis for Heap-Directed Pointers in C," Rakesh Ghiya and Laurie J. Hendren, in Conference Record of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, Florida, pp. 1-15, January 1996.
  • Supplemental readings:
  • Oct 15 Midterm
    Oct 17 Is Code Optimization Relevant?
    Oct 22
  • Pointer Analysis: Haven't We Solved This Problem Yet? Michael Hind 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE'01), Snowbird, Utah, June 18-19, 2001. (Slides)
  • Efficient Context-Sensitive Pointer Analysis For C Programs, Bob Wilson and Monica Lam, Proceedings of the ACM SIGPLAN'95 Conference on Programming Language Design and Implementation, 1995.
  • Oct 24
  • Points-to Analysis in Almost Linear Time, Bjarne Steensgaard, Proceedings of the Twentythird Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1996.
  • Unification-Based Pointer Analysis with Directional Assignments, Manuvir Das, PLDI '00: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, Vancouver, BC, Canada, June 2000.
  • Oct 29
  • Bacon paper
  • Program extraction
  • Fast Static Analysis of C++ Virtual Function Calls , D. Bacon and P. Sweeney OOPSLA'96 Conference Proceedings: Object-Oriented Programming Systems, Languages , and Applications, ACM SIGPLAN Notices volume 31 number 10, San Jose, California, October 1996.
  • Fast Interprocedural Class Analysis, Greg DeFouw, David Grove, and Craig Chambers, In Conference Record of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1998.
  • Oct 31
  • GC notes by Alexander Mosolov
  • GC notes by Bogdan Stroe
  • Garbage collection
  • Animation of Cheney algorithm
  • Powerpoint Show on Garbage Collection by Richard Jones
  • Uniprocessor Garbage Collection Techniques, Paul Wilson, International Workshop on Memory Management, 1992.
  • Nov 5
  • An API for Runtime Code Patching, by Bryan Buck and Jeffrey K. Hollingsworth.
  • Efficient Instrumentation for Code Coverage Testing, M. Tikir and J. K. Hollingsworth ISSTA'02 July 2002.
  • Nov 7
  • Diduce Notes by Zhongchao Yu
  • Diduce Notes by Jeff Odom
  • ``Dynamically Discovering Likely Program Invariants to Support Program Evolution''M by Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin. IEEE Transactions in Software Engineering, v27#2, Feb 2001, pp 1-25.
  • Tracking Down Software Bugs Using Automatic Anomaly Detection, Sudheendra Hangal and Monica S. Lam, In Proceedings of the International Conference on Software Engineering, pages 291-301, May 2002.
  • Nov 12
  • Notes by Nathaniel Waisbrot
  • Lecture notes
  • Notes by Walid Gomaa
  • Notes by Ruggero Morselli
  • Type-Based Analysis and Applications Jens Palsberg, PASTE 2001 (Slides)
  • Lackwit: A Program Understanding Tool Based on Type Inference, Robert O'Callahan and Daniel Jackson, International Conference on Software Engineerin g, 1997.
  • Nov 14
  • Tsz-Chiu's collection of links on model checking
  • Merz's slides on model checking
  • Slides on Bandera
  • Bandera notes by Steve Haga
  • Model Checking: A Tutorial Overview Stephan Merz, Modeling and Verification of Parallel Processes. LNCS 2067, Springer-Verlag
  • Bandera : Extracting Finite-state Models from Java Source Code, James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, Hongjun Zheng in Proceedings of the 22nd International Conference on Software Engineering, June, 2000.
  • Nov 19
  • Notes by Austin Parker
  • Foundational Calculi for Programming Languages
  • Lecture notes on the Pi Calculus
  • Lecture notes on CCS
  • Types as Models
  • Types as Models: Model Checking Message-Passing Programs, Sagar Chaki, Sriram K. Rajamani and Jakob Rehof Proceedings POPL 02, 29th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages, Portland, January 16-18, 2002.
  • Modern Concurrency Abstractions for C#, Nick Benton, Luca Cardelli, Cedric Fournet.
  • Nov 21
  • Example of Prefix output
  • Prefix notes by Minkyoung Cho
  • Prefix slides by Minkyoung Cho
  • Prefix notes by Nikhil Swamy
  • Prefix notes by Matthew Snover
  • ESC-java notes by Che-Rung Lee
  • ESC-java notes by Weihan Huang
  • A Static Analyzer for Finding Dynamic Programming Errors, William R. Bush, Jonathan D. Pincus and David J. Sielaff, Software--Practice and Experience , 2000.
  • Extended static checking for Java Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe and Raymie Stata, PLDI 2002
  • Nov 26
  • Notes by Abheek Anand
  • PLDI 2002 presentation
  • Lecture notes
  • A system and language for building system-specific, static analyses, Seth Hallem, Benjamin Chelf, Yichen Xie, and Dawson Engler, PLDI 2002
  • Dec 3
  • Notes by Vasile Bagurici on predicate abstraction
  • Notes by John Rose on Mining Specifications
  • Notes by Feng Peng on Mining Specifications "
  • PLDI 2001 presentation of Automatic Predicate Abstraction of C Programs
  • High level overview of Mining Specifications
  • Detailed discussion of Mining Specifications
  • Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd Millstein and Sriram Rajam, In Proceedings of the SIGPLAN C onference on Programming Language Design and Implementation, 2001.
  • Mining Specification, Glenn Ammons and Rastislav Bodik and James R. Larus, To appear at Principles of Programming Languages (POPL02), Portland, Oregon, 16- 18 January 2002
  • Dec 5 Snow day
    Dec 10
  • Notes on Lerner et al. by Konstantinos Bitsakos
  • Notes on Lernet et al. by Polyvios Pratikakis
  • Slides on Lerner et al. by John Jorgensen, McGill
  • ICSE slides on ArchJava
  • OOPSLA slides on AliasJava
  • Notes on AliasJava by Daniel Khodorkovsky
  • Composing Dataflow Analyses and Transformations, Sorin Lerner, David Grove and Craig Chambers, Principles of Programming Languages (POPL02), Portland, Oregon, 16- 18 January 2002
  • Alias Annotations for Program Understanding, Jonathan Aldrich, Valentin Kostadinov, and Craig Chambers The Conference on Object-Oriented Programming Systems, Languages, and Applicatio ns (OOPSLA '02), Seattle, Washington, November 4-8, 2002.
  • ArchJava: Connecting Software Architecture to Implementation, Jonathan Aldrich, Craig Chambers, and David Notkin, The International Conference on Software Engineering (ICSE '02), Orlando, Florid a, May 19-25, 2002.
  • Dec 12
  • Notes on AspectJ by Tai Hu
  • Notes on AspectJ by David Greenfield
  • Example by David Greenfield:
  • An Overview of AspectJ, Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm and William G. Griswold. In ECOOP 2001.
  • Maya: multiple-dispatch syntax extension in Java Jason Baker and Wilson C. Hsieh, PLDI 2002
  • Papers

    Papers for the rest of the semester will be selected from this list.


    Home works / Programming Assignments

    1. Sets and Graphs in O'Caml, due Sep 20th, 6pm
    2. Dataflow analysis using MURZ, due Oct 8th, 6pm
    3. Read a paper deeply, read related work, help in presentation, write a 1-2 page report.




    ICFP Programming contest


    As usual, everything is subject to change

    • Types
      • Basic simple type systems
      • Type inference
      • Parametric polymorphism
      • Inclusion polymorphism (subtyping)
        • Inheritence
        • Object type systems
      • Typed assembly language
    • Dataflow analysis
      • Def-use chains
      • Static single assignment form
      • Dominators
      • Abstract interpretation
      • Various program control/data flow graphs
    • Pointer analysis
    • Logical systems
      • Theorem proving
      • Proof checking (e.g., Proof carrying code)
      • User annotations (e.g., Extended static checking)
    • Model checking
    • Constraint-based analysis
      • 0CFA
      • Set-based analysis
      • Label flow
        • CFL reachability
      • Alias analysis
      • Soft typing
  • Functional / Higher order programming
    • ML
    • Haskell
  • Object Oriented Programming
    • Squeak
    • GJ (a.k.a. Java 1.5)
    • Cecil
  • Bug detection
    • Buffer overflows
    • Format string bugs
    • Y2K
  • Static Analysis tools
    • LCLint
    • Meta-level compilation
    • SLAM
  • Typical Grading and Workload

    The course will be graded based on homeworks (including programming projects) and exams. There will not be substantial group projects.