Analyis And Verification of Software

Spring 2014

prof. A. Cortesi

Reference books

Lecture notes - 2014

  1. (03.02.2014) Introduction to Static Analysis Techniques: Approach and Use(pdf)
  2. (07.02.2014) Program Optimizations (pdf)
  3. (10.02.2014) Partial orders, Lattices, etc. (pdf)
  4. (14.02.2014) Dataflow Analysis: Reaching Definitions (pdf)
  5. (17.02.2014) Dataflow Analysis: Liveness, Available Expressions, etc. (pdf)
  6. (21.02.2014) No lecture today
  7. (24.02.2014) Dataflow Analysis: a General Framework (pdf)
  8. (27.02.2014) Dataflow Analysis: non-distributive properties - Interprocedural Analysis (pdf)
  9. (03.02.2014) No lecture today
  10. (07.02.2014) Abstract Interpretation: a gentle introduction(pdf)
  11. (10.03.2014) Abstract Interpretation: concrete and abstract semantics (pdf)
  12. (14.03.2014) Abstract Interpretation: concrete and abstract semantics (ctd.) (pdf)
  13. (17.03.2014) Abstract Interpretation: fixpoint computation, widening and narrowing (pdf)
  14. (21.03.2014) Abstract Interpretation: combining domains by product operators (pdf)
  15. (24.03.2014) No lecture today
  16. (28.03.2014) Model Checking: Automata and Temporal Logic Formulas (pdf)
  17. (31.03.2014) No lecture today
  18. (04.04.2014) Model Checking: Temporal Logics (pdf)
  19. (07.04.2014) Model Checking: Fixpoint Computation (pdf). Conclusions (pdf)


  1. The first homework, on lattices and continuous functions, is due by february 17, 2014 (see the wiki area)
  2. The second homework, on copy propagation analysis, is due by february 28, 2014
  3. The third homework, on interval analysis, is due by apri 4, 2014
  4. The fourth homework, on model checking, is due by apri l8, 2014

Final Project: Static Analysis of Android apps

  1. To do in groups (two to four students)
  2. Get familiar with Android development tools
  3. Get the “state of the art” in the scientific literature
  4. Focus on properties that may be useful to verify (possibly non-functional properties of apps, like security properties)
  5. Design a suite of case studies (code, property, expected result), select an appropriate static analysis technique, define the analysis in formal way, and apply it “by hands” on the case studies.
  6. Reference material is posted in the wiki area