Analyis And Verification of Software

Spring 2015

prof. A. Cortesi

Reference books


Lecture notes - 2015

  1. (02.02.2015) Introduction to Static Analysis Techniques: Approach and Use(pdf)
  2. (03.02.2015) Tour of common optimizations(pdf)
  3. (09.02.2015) Partial orders, Lattices, Continuous Functions, Fixpoints (pdf)
  4. (10.02.2015) Dataflow Analysis: Reaching Definitions (pdf)
  5. (23.02.2015) Dataflow Analysis: Liveness (pdf)
  6. (24.02.2015) Available Expressions, Very Busy Expressions, General DFA Framework (pdf)
  7. (02.03.2015) Non-Distributive Analyses - Inter-procedural Analysis (pdf)
  8. (03.03.2015) Abstract Interpretation: an Overview (pdf)
  9. (09.03.2015) Concrete and Abstract Semantics (pdf)
  10. (10.03.2015) Concrete and Abstract Semantics (ctd.)(pdf)
  11. (16.03.2015) Widening and Narrowing Operators(pdf)
  12. (17.03.2015) Product Operators (pdf)
  13. (23.03.2015) Datacentric Semantics for Privacy Policies Compliance Verification (pdf)
  14. (24.03.2015) Model Checking: Automata (pdf)
  15. (30.03.2015) Model Checking: Temporal Logics (pdf)
  16. (31.03.2015) Seminar (Enrico Steffinlongo)

Homeworks

  1. (03.02.2015) Homework 1(pdf)
  2. (10.02.2015) Homework 2(pdf)
  3. (24.02.2015) Homework 3(pdf)
  4. (10.03.2015) Homework 4(pdf)

  5. A simple overview of domains (and in particular of the congruence domain) can be found here.