CSE6049
CSE6049 Program Analysis
News
- Check out your score of final exam link sol
- Check out your score of HW 4: link
- Check out your score of HW 3: link
- HW4 is out! (due: 06/09 (Wed))
- The due date for HW3 is extended to 5/17 (Mon).
- Scores of HW 1 & 2 (links to the solutions can be found below): link
- HW3 is out! (due: 05/10 (Mon))
- HW2 is out! (due: 04/19 (Mon))
- HW1 is out! (due: 04/05 (Mon))
- How to setup OcaIDE on Windows: link
- Video lectures will be provided (available on HY-ON LMS).
Basic Information
- Instructor: Woosuk Lee
- Office Location: Rm#403, Eng. Bldg 3
- Telephone: 031-400-1031
- Email: woosuk at hanyang.ac.kr
- Office Hours: Friday 10:00 - 12:00
- Time
- Monday 17:30 - 19:00
- TA
- Baljiniam Bassan Ochir (Baska) (email: bbumbuul at yahoo.com)
References
- The course textbook: Introduction to Static Analysis: An Abstract Interpretation Perspective by Xavier Rival and Kwangkeun Yi
- Materials from related courses: Program Analysis: Theories and Practices at Seoul Nat’l Univ.
Slides & Course Schedule (tentative)
- Course Overview: pdf
- Preliminary Concepts (1): Inductive Definitions, Denotational Semantics: pdf
- Preliminary Concepts (2): Functional Programming: pdf1 pdf2
- Preliminary Concepts (3): Operational Semantics, Interpreters: pdf code1 code2
- A Gentle Introduction to Static Analysis (1): pdf
- A Gentle Introduction to Static Analysis (2): pdf
- Abstract Interpretation Framework: pdf
- General Static Analysis Framework based on a Compositional Semantics: pdf
- General Static Analysis Framework based on a Transitional Semantics: pdf
- Advanced Static Analysis Technique: pdf
- Static Analysis for Advanced Programming Feature: pdf
- Specialized Static Analysis Framework: Datalog analysis: pdf
- Specialized Static Analysis Framework: Type inference: pdf
Grading
- Homework: 65%
- Final exam: 25%
- Attendance: 10%
Reating Material
Reading material related to the lesson
- Introduction to Software Analysis
- What is static program analysis? talk by Matthew Might.
- Explains why program analysis is undecidable and develops a static analysis to play with in Racket.
- Lessons from Building Static Analysis Tools at Google
- Describes experiences developing and deploying program analysis tools at Google.
- What Developers Want and Need from Program Analysis: An Empirical Study
- One of the best empirical studies about program analysis.
- The Coming Software Apocalypse
- Overview of the state of software reliability problems and solutions to overcome them.
- From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis
- Describes experiences developing and deploying program analysis tools at Facebook.
- What is static program analysis? talk by Matthew Might.
- Pointer Analysis
- Pointer Analysis, Foundations and Trends in Programming Languages, 2015
- Recent survey of pointer analysis.
- Pointer Analysis, Foundations and Trends in Programming Languages, 2015
- Inter-Procedural Analysis
- Undecidability of Context-Sensitive Data-Dependence Analysis, ACM TOPLAS, 2000
- Proof of undecidability of tracking calls/returns and reads/writes simultaneously.
- Undecidability of Context-Sensitive Data-Dependence Analysis, ACM TOPLAS, 2000
- Abstract Interpretation
- Abstract Interpretation Based Formal Methods and Future Challenge
- A good overview of Abstract Interpretation framework
- Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation
- An interesting theorem about the power of widening and narrowing
- Design and Implementation of Sparse Global Analyses for C-like Languages
- Describes how to accelerate existing static analyses without precision loss
- A Static Analyzer for Large Safety-Critical Software
- Describes how to apply abstract interpretation into formal verification of AirBus software
- Abstract Interpretation Based Formal Methods and Future Challenge
- Type Systems
- Type Systems, CRC Handbook, 2004