This course will focus on static and dynamic program analysis techniques that can be used to perform tasks such as program
verification, profiling, optimization, repair, and comprehension. The students will learn the concepts behind the techniques, and will
apply their learning to develop analyses using the state-of-art tools. Ensuring program correctness can be very challenging.
Programmers depend on testing to build some confidence in the expected behavior of programs. Although testing is essential, the
complexity as well as the criticality of modern software demands more rigorous techniques, in addition to testing, to ensure software
correctness. The properties that programs need to satisfy vary from safety properties to security properties and in terms of expressiveness from simple predicates that check the program states at specific execution points to regular expressions and context-free grammars that check the legality of traversed program paths. In this course, we will focus on program verification and the
students will learn about static analysis techniques, i.e., the techniques that can be applied to programs without running the programs as well as about dynamic analysis (or runtime monitoring) techniques that analyze programs during runtime. The students will learn about the strengths and weaknesses of both techniques. In the static analysis, we will primarily focus on dataflow analysis, and learn about some standard analyses that are used in program verification and optimization. However, the course will also introduce students to some advanced static analysis topics such as symbolic execution, and will cover some topics related to security analysis.
We will primarily use Java as programming language and "Soot" as a static analysis tool. In the dynamic analysis part, the students
will learn to specify properties of interest mainly using regular expressions and finite state automata, and use aspects to build runtime monitors to check those properties. In the process, they will learn to develop “aspects” to instrument and monitor programs.
Implement a dataflow analysis using Soot static analyzer.
Implement a simple flow-sensitive inter-procedural analysis.
Use a symbolic execution tool to generate test cases.