Advanced course: Program analysis and verification
Admin
- Lecturer: Noam Rinetzky
- Time: Thursday, 9:00–12:00, Semester B, 2015/16
- Location: Schreiber 008
- Reception Hour: Set by Email
- Course Number: 0368-4479
Assignments and grades
- 2-3 theoretical assignments (35% of the course grade)
- 1 practical assignment (15% of the course grade)
- A final project (50% of the course grade)
- No final exam
Lectures
| Date | Topic | Slides | |
|---|---|---|---|
| 29-February-2016 | Overview | PPTX 1 | PDF 1 |
| 07-March-2016 | Operational Semantics | PPTX 2 | PDF 2 |
| 14-March-2016 | Axiomatic Semantics | PPTX 3 | PDF 3 |
| 21-March-2016 | Axiomatic Semantics | PPTX 4 | PDF 4 |
| 28-March-2016 | Axiomatic Semantics | PPTX 4 (cont.) | PDF 4 (cont.) |
| 4-April-2016 | Rely/Guarantee | PPTX 5 | PDF 5 |
| 4-April-2016 | Abstract Interpretation | PPTX 6 | PDF 6 |
| 11-April-2016 | Abstract Interpretation | PPTX 7 | PDF 7 |
| 2-May-2016 | Abstract Interpretation | PPTX 8 | PDF 8 |
| 16-May-2016 | Abstract Interpretation + Pointer Analysis | PPTX 9 | PDF 9 |
| 23-May-2016 | Shape Analysis | PPTX 10 | PDF 10 |
| 30-May-2016 | Interprocedural (Shape) Analysis | PPTX 11 | PDF 11 |
| 1-June-2016 | Verification Day -- Wednesday! | Program + Slides | |
| 6-June-2016 | Numerical Analysis + LLVM | PPTX 12 | PDF 12 |
Home Assignments
Resources
- An online version of the Semantics with Applications book by Nielson and Nielson
- A book about static analysis Principles of Program Analysis (hard copy vailable in the library).
- A LaTeX package for typesetting inference rules.
- Mathematical fonts for Powerpoint and Word can be found here.