Advanced course: Program analysis and verification

Admin

  • Lecturer: Noam Rinetzky
  • Time: Thursday, 9:00–12:00, Semester B, 2017/18
  • Location: Dan David 201
  • 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) -- to be submitted by 31/Aug/2018
  • No final exam

Lectures

  • Lecture 1: Overview + Natural Operational Semantics
    • Date: 5/March/2018
    • Slides: PPTX
  • Lecture 2: Structural Operational Semantics + Symbolic Execution
    • Date: 12/March/2018
    • Slides: PPTX (OS)
    • Slides: PDF (SE)
  • Lecture 3: Axiomatic Semantics
    • Date: 19/March/2018
    • Slides: PPTX
  • Lecture 4: Abstract Interpretation (Basic)
    • Date: 9/April/2018
    • Slides: PPTX
  • Lecture 5: Abstract Interpretation (Galois Connections)
    • Date: 16/April/2018
    • Slides: PPTX PDF
  • Lecture 6: Abstract Interpretation (Composing Abstract Domains)
    • Date: 23/April/2018
    • Slides: PPTX PDF
  • Lecture 7: Abstract Interpretation (Numerical Analysis)
    • Date: 30/April/2018
    • Slides: PPTX PDF
  • Lecture 8: Interproceural Analysis + Pointer Analysis
    • Date: 7/May/2018
    • Slides: PPTX PDF
  • Lecture 9: Shape Analysis
    • Date: 7/May/2018
    • Slides: PPTX PDF
  • Lecture 10: Shape Analysis
    • Date: 21/May/2018
    • Slides: PPTX PDF
  • Lecture 11: Interprocedural Shape Analysis
    • Date: 27/May/2018
    • Slides: PPTX PDF
  • Lecture 12: Separation Logic
    • Date: 4/June/2018
    • Slides: in Moodle

Home Assignments

  1. Ex 1
  2. Ex 2

Resources