One can ask many interesting questions about a given program such as:
- Can the pointer 'p' be 'null'?
- Do the variables 'x' and 'y' point to the same location in memory?
- Could the secret data pointed to by 's' leak to some unauthorized party?
Answering those questions is undecidable as stated by Rice's Theorem. However, program analysis can provide approximate answers to those questions, which works well in many cases. For example, many bug finding tools (e.g., FindBugs) use various program analysis techniques to detect, and possibly fix, bugs in a given program. Additionally, security analysis tools (e.g., AppScan, FlowDroid) also use program analysis to detect security vulnerabilities and data leaks.
This course will introduce the main concepts behind program analysis, give an overview of the program analyses that work and those that do not work in practice, and discuss how to design program analyses for modern software systems.
- Apply mathematical abstractions (e.g., lattices and fixpoints) to writing complex software.
- Understand basic call graph analyses and advanced pointer analyses.
- Acquire basic knowledge about formal program analysis frameworks (e.g., IFDS, IDE).
- Have a strong command of various analysis tools such as Soot, WALA, and DOOP.
- Understand the basic concepts behind formal proofs in the field of programming languages.
- Engage in a discussion about research papers in the field of programming languages.
- Team Project