Program Analysis: 2015-2016
Lecturer | |
Degrees | Schedule C1 (CS&P) — Computer Science and Philosophy Schedule C1 — Computer Science |
Term | Hilary Term 2016 (18 lectures) |
Overview
Program analyses are techniques for automatically discovering information about programs, usually without running programs explicitly. The area of program analysis originally started with the humble goal of finding simple program properties and aiding compiler optimisations. However, in the past fifteen years, it has made noticeable progress, and produced effective algorithms for discovering challenging program properties and enabling a new type of ambitious applications on software, such as automated software verification, security analysis, and program synthesis. In this course, we will cover important program-analysis techniques, in particular those developed in the past fifteen years, discuss general principles behind these techniques, and look at recent development that combine these principles with the ideas from different research areas. Throughout the course, we will emphasise both thorough theoretical understanding of program-analysis techniques and hands-on experience with building tools based on these techniques.Prerequisites: We do not require any prerequisite courses. However, we recommend students to take Compilers before taking this course, if it is possible. Throughout the course, we assume that students are familiar with basic concepts from Discrete Math, such as set and partial order, and have experience with using Hoare logic and invariants for proving programs from Imperative Programming or some similar courses. Also, this course covers materials from recent research, so students should feel comfortable with learning from less organised sources, such as research papers. Finally, practical problems will be based on the Soot framework (http://sable.github.io/soot/) and be done in the Scala or Java programming language.
Learning outcomes
After completing this course, students will be able to develop effective program analysers for their own problems. This means that the students will understand key ideas behind program-analysis techniques, gain intuition on the kind of problems where these ideas can be applied effectively, and learn how to exploit existing frameworks for building program analysis tools.Synopsis
- Overview.
- Lattice theory and abstract interpretation.
- Interval analysis and non-relational program analysis.
- Introduction to the Soot framework.
- Octagon analysis and relational program analysis.
- Pointer analysis and heap abstraction.
- Techniques for transforming or combining abstract domains.
- Interprocedural program analysis.
- Abstraction refinement.
- Data-driven program analysis.
Reading list
Nielson et al's textbook is a good reference on the topics covered in the paper, although the course does not follow the textbook:
- Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis. Springer (Corrected 2nd printing, 452 pages, ISBN 3-540-65410-0), 2005.
We give a tentative list of research papers related to the materials covered in the course. During lectures, we will select some in the list and add other papers and suggest students to read them.
- Abstract Interpretation:
- Patrick Cousot, Radhia Cousot: Abstract Interpretation Frameworks. J. Log. Comput. 2(4): 511-547 (1992)
- Patrick Cousot, Radhia Cousot: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL 1977: 238-252
- Patrick Cousot, Radhia Cousot: Systematic Design of Program Analysis Frameworks. POPL 1979: 269-282
- Francois Bourdoncle: Efficient Chaotic Iteration Strategies with Widenings. In Proceedings of 1993 International Conference on Formal Methods in Programming and their Applications.
- Soot tutorials: See https://github.com/Sable/soot/wiki/Tutorials.
- Numerical abstract domains:
- Antoine Mine: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1): 31-100 (2006)
- Francesco Logozzo, Manuel Fahndrich: Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. Sci. Comput. Program. 75(9): 796-807 (2010)
- Patrick Cousot, Nicolas Halbwachs: Automatic Discovery of Linear Restraints Among Variables of a Program. POPL 1978: 84-96
- Interprocedural analyses:
- Thomas W. Reps, Susan Horwitz, Shmuel Sagiv: Precise Interprocedural Dataflow Analysis via Graph Reachability. POPL 1995: 49-61
- Yannis Smaragdakis, Martin Bravenboer, Ondrej Lhotak: Pick your contexts well: understanding object-sensitivity. POPL 2011: 17-30
- Pointer analysis and heap abstraction:
- Bjarne Steensgaard: Points-to Analysis in Almost Linear Time. POPL 1996: 32-41
- Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm: Parametric Shape Analysis via 3-Valued Logic. POPL 1999: 105-118
- Dino Distefano, Peter W. O'Hearn, Hongseok Yang: A Local Shape Analysis Based on Separation Logic. TACAS 2006: 287-302
- Abstraction refinement:
- Thomas Ball, Sriram K. Rajamani: The SLAM project: debugging system software via static analysis. POPL 2002: 1-3
- Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith: Counterexample-Guided Abstraction Refinement. CAV 2000: 154-169
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244
- Andrey Rybalchenko, Viorica Sofronie-Stokkermans: Constraint Solving for Interpolation. VMCAI 2007: 346-362
- Xin Zhang, Mayur Naik, Hongseok Yang: Finding optimum abstractions in parametric dataflow analysis. PLDI 2013: 365-376
- Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, Hongseok Yang: On abstraction refinement for program analyses in Datalog. PLDI 2014: 27
- Application of machine learning in program analysis:
- Veselin Raychev, Martin T. Vechev, Andreas Krause: Predicting Program Properties from "Big Code". POPL 2015: 111-124
- Hakjoo Oh, Hongseok Yang, Kwangkeun Yi: Learning a strategy for adapting a program analysis via Bayesian optimisation, 2015
Feedback
Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.
Taking our courses
This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses
Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.