Program Analysis

Module aims

The course will provide you with an introduction to the areas of classical and probabilistic program analysis.
Starting from methods used in compiler optimisation (Live Variable, etc.) you will be introduced to lattice based approaches to Data-flow Analysis (Monotone Frameworks) and Control-flow Analysis before we discuss the general, semantics based framework of Abstract Interpretation.
Considering quantitative properties of (probabilistic) programs you will then see how to extend classical program analysis to this setting. This leads to a framework of Probabilistic Abstract Interpretation which is based to an appropriate formal semantics.

Learning outcomes

Upon successful completion of this module you will be able to:
- design classical program analysis, such as data-flow and control-flow, for classical and probabilistic programs
- solve the equations and constraints resulting from program analysis
- reason informally about the complexity of constraint solving algorithms
- specify formally the classical and probabilistic properties of programs based on their semantics
- reason about the correctness of a given program analysis on the basis of the semantics of the program

Module syllabus

- Static Program Analysis
- Operational Semantics and Traces
- Dataflow Analysis (for imperative programs)
- Program Properties (Lattices)
- Monotone Frameworks
- Control Flow Analysis (for functional programs)
- Abstract Interpretation (Galois Connections)
- Compositional Probabilistic Models (Tensor Product)
- Order Reduction and Simplification
- Probabilistic Abstract Interpretation (Moore-Penrose, Pseudo-Inverse)
- Applications: Probabilistic Dataflow Analysis, Bisimulation, etc.
- Optional: Relation to machine learning (Least Square Approximation)
- Optional: Construction of Optimal Abstractions

Teaching methods

The material will be taught through traditional lectures, exercises in class, backed up by unassessed, formative, exercises designed to reinforce the taught material.   

Assessments

Regular sets of formative exercises will be provided to reinforce your understanding of the material taught. There will be two tests in class that contribute 20% of the mark for the module. There will be a final written exam, which counts for the remaining 80% of the marks.

Feedback on formative exercises will be given in class. Written feedback will be given on the tests and exam. This will be returned within two weeks after the tests.   

Reading list

Core reading

Module leaders

Dr Herbert Wiklicky

 

View the module reading list (Leganto)