Analyis And Verification of Software

Spring 2013

prof. A. Cortesi

• F.Nielson, H.R.Nielson, C. Hankin: Principles of Program Analysis, Springer Verlag, 2004
• B.Berard et al., Systems and Software Verifications. Springer Verlag 2001.

1. (08.02.2013) Introduction to Static Analysis Techniques: Approach and Use(pdf)
2. (15.02.2013) Program Optimizations (pdf)
3. (18.02.2013) Dataflow Analysis: Reaching Definitions(pdf)
4. (22.02.2013) Dataflow Analysis: Liveness, Available Expressions, Very Busy Expressions(pdf)
5. (25.02.2013) Dataflow Analysis: Towards a General Framework (pdf)
6. (01.03.2013) Dataflow Analysis: Inter-procedural Analysis (pdf)
7. (04.03.2013) Abstract Interpretation: a gentle introduction (pdf)
8. (08.03.2013) Abstract Interpretation: concrete and abstract semantics (pdf)
9. (11.03.2013) Abstract Interpretation: concrete and abstract semantics for recursion (pdf)
10. (15.03.2013) Abstract Interpretation: fixpoint computation and widening (pdf)
11. (18.03.2013) Abstract Interpretation: product operators (pdf)
12. (22.03.2013) Model Checking: Kripke Models (pdf)
13. (25.03.2013) Model Checking: Temporal Logics (pdf)
14. (08.04.2013) Model Checking: Fixpoint Computation (pdf)
15. (15.04.2013) Summary and Research Perspectives (pdf)

1. (by 14.03.2013) Homework 1: Dataflow Analysis
2. (by 18.04.2013) Homework 2: Abstract Interpretation
3. (by 10.05.2013) Homework 2: Model Checking

1. (by 30.09.2013 at most) Description: see the last slide of the last lecture.
   Materials: see here