E0 227 Program Analysis and Verification

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 sub-disciplines 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 day-to-day 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
  1. 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].
     • Byte-code verification [leroy01].
     • SAL and ESPx [espx06]
     • Cqual [cqual_toplas].
     • SLAM and Static Driver Verifier [sdv06].
     • Spec# and Boogie [specsharp04,boogie05].
     • Saturn.
     • BDDBDDB [whaley05]

  2. Type Checking and Type State Verification (Sriram):
     • Standard type checking and type inference
     • Specifying type systems using datalog
     • Non-standard 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]
     • Type-based pointer analyses [das00,antgrass07,sridharan06]

  3. Dataflow analysis (Deepak):
     • global program optimization [kildall73]
     • Context-sensitive 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]

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

  5. Model checking (Aditya):
     • Push down model checking
     • Abstraction refinement
     • SLAM, BLAST and MOPS (Hao Chen's tool)

  6. 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
  1. Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis, Springer, 1999.
  2. Benjamin Pierce: Foundational Calculi for Programming Languages, CRC Handbook of Computer Sc and Engineering, 1995.
  3. [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 43--48, 2007.
  4. [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 597--604, New York, NY, USA, 1968. ACM Press.
  5. [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 73--85, New York, NY, USA, 2006. ACM Press.
  6. [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 safety-critical software.
     In PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pages 196--207, New York, NY, USA, 2003. ACM Press.
  7. [boogie05] Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.
     Boogie: A modular reusable verifier for object-oriented programs.
     In FMCO, volume 4111 of Lecture Notes in Computer Science, pages 364--387, 2005.
  8. [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 49--69, 2005.
  9. [bryant92] Randal E. Bryant.
     Symbolic boolean manipulation with ordered binary-decision diagrams.
     ACM Comput. Surv., 24(3):293--318, 1992.
  10. [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 SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238--252, New York, NY, USA, 1977. ACM Press.
  11. [cc79] Patrick Cousot and Radhia Cousot.
      Systematic design of program analysis frameworks.
      In POPL '79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 269--282, New York, NY, USA, 1979. ACM Press.
  12. [halbwachs78] Patrick Cousot and Nicolas Halbwachs.
      Automatic discovery of linear restraints among variables of a program.
      In POPL, pages 84--96, 1978.
  13. [chaka03] Venkatesan T. Chakaravarthy.
      New results on the computability and complexity of points--to analysis.
      In POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 115--125, New York, NY, USA, 2003. ACM Press.
  14. [das00] Manuvir Das.
      Unification-based pointer analysis with directional assignments.
      In PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, pages 35--46, New York, NY, USA, 2000. ACM Press.
  15. [vault] Robert DeLine and Manuel Fahndrich.
      Enforcing high-level protocols in low-level software.
      In PLDI, pages 59--69, 2001.
  16. [simplify05] David Detlefs, Greg Nelson, and James B. Saxe.
      Simplify: a theorem prover for program checking.
      J. ACM, 52(3):365--473, 2005.
  17. [cqual_toplas] Jeffrey S. Foster, Robert Johnson, John Kodumal, and Alex Aiken.
      Flow-insensitive type qualifiers.
      ACM Trans. Program. Lang. Syst., 28(6):1035--1087, 2006.
  18. [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 133--144, New York, NY, USA, 2006. ACM Press.
  19. [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 376--386, New York, NY, USA, 2006. ACM Press.
  20. [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 232--241, New York, NY, USA, 2006. ACM Press.
  21. [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 290--299, New York, NY, USA, 2007. ACM Press.
  22. [hoarecacm69] C. A. R. Hoare.
      An axiomatic basis for computer programming.
      Commun. ACM, 12(10):576--580, 1969.
  23. [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 SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pages 13--19, New York, NY, USA, 2005. ACM Press.
  24. [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 207--218, New York, NY, USA, 2004. ACM Press.
  25. [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 169--179, New York, NY, USA, 1970. ACM Press.
  26. [kildall73] Gary A. Kildall.
      A unified approach to global program optimization.
      In POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 194--206, New York, NY, USA, 1973. ACM Press.
  27. [king76] James C. King.
      Symbolic execution and program testing.
      Commun. ACM, 19(7):385--394, 1976.
  28. [leroy01] Xavier Leroy.
      Java bytecode verification: An overview.
      In CAV, volume 2102 of Lecture Notes in Computer Science, pages 265--285, 2001.
  29. [landi91] William Landi and Barbara G. Ryder.
      Pointer-induced aliasing: a problem taxonomy.
      In POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 93--103, New York, NY, USA, 1991. ACM Press.
  30. [whaley05] Monica S. Lam, John Whaley, V. Benjamin Livshits, Michael C. Martin, Dzintars Avots, Michael Carbin, and Christopher Unkel.
      Context-sensitive program analysis as database queries.
      In PODS '05: Proceedings of the twenty-fourth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, pages 1--12, New York, NY, USA, 2005. ACM Press.
  31. [muth00] Robert Muth and Saumya Debray.
      On the complexity of flow-sensitive dataflow analyses.
      In POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 67--80, New York, NY, USA, 2000. ACM Press.
  32. [dbm01] Antoine Min{\'e}.
      A new numerical abstract domain based on difference-bound matrices.
      In PADO, pages 155--172, 2001.
  33. [cfl_reach95] Thomas Reps, Susan Horwitz, and Mooly Sagiv.
      Precise interprocedural dataflow analysis via graph reachability.
      In POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 49--61, New York, NY, USA, 1995. ACM Press.
  34. [sridharan06] Manu Sridharan and Rastislav Bod\'{\i}k.
      Refinement-based context-sensitive points-to analysis for java.
      In PLDI, pages 387--400, 2006.
  35. [Tarski55] Alfred Tarski:
      A lattice-theoretic fixpoint theorem and its applications, Pacific J. Mathematics, 5, pages 285--309, 1955.

• Lecture slides:
  • Overview Lecture 1, zipped version.
  • Overview of tools
    • Lecture 2, zipped version.
    • Lecture 3, zipped version.
    • Lecture 4, zipped version.
  • Typing
    • Lecture 5, zipped version.
    • Lecture 6, zipped version.
    • Lecture 7, zipped version.
    • Lecture 8, zipped version.
    • Lecture 9, zipped version.
  • Data Flow Analysis
    • Lecture 10, zipped version.
    • Lecture 11&12
    • Lecture 13&14
    • Lecture 21&22
    • Lecture 15 (Cloning analysis).
  • Assertion-Based Reasoning
    • Lecture 16.
    • Lecture 17.
    • Lecture 18.
    • Lecture 19.
    • Lecture 20.
  • Abstract Interpretation Lectures 23&24.
  • Model Checking
    • Lectures 23&24.
    • Lecture 25.
  • Logical Abstract Interpretation (Sumit Gulwani)
    • Lectures.
    • Assignment.

• Lecture notes (scribed by Arnab De and K R Raghavendra) last updated on 26 Sept 2007.

• Assignments
  • Assignment 1 due on Thu 23 August 2007.
  • Assignment 2 due on Thu 20 September 2007.
  • Assignment 3 due on Wed 19 September 2007.
  • Assignment 4 due on Tue 23 October 2007.
  • Assignment 5 due on Mon 19 November 2007.
  • Question Sheet on data-flow analysis.

• Weightage for evaluation:
  • Assignments (Lab + written) + Seminar: 60%
  • Final Exam: 40%

• Current meeting schedule: Mon, Wed 10:00am, in E-Classroom, CSA Dept. Tutorial/Seminar slot: Thu 10:00am in E-Classroom.

• Weightage for evaluation:
  • Assignments (Lab + written) + Seminar: 60%
  • Final Exam: 40%

• Current meeting schedule: Mon, Wed 10:00am, in E-Classroom, CSA Dept. Tutorial/Seminar slot: Thu 10:00am in E-Classroom.

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