| 1 |
Lecture: Course Overview and Introduction Lab: C++ Practices, Graph Algorithms, Vulnerability |
Configure IDE |
Lab-Exercise-1 |
|
| 2 |
Lecture: LLVM, SVFIR and Control-Flow Lab: Code Graphs, Control-Flow Reachability |
LLVM-IR SVF-IR SVF APIs |
|
Assignment-1 |
| 3 |
Lecture: Data-Flow and Taint AnalysisLab: Information Flow Tracking |
|
|
|
| 4 |
Lecture: Code Verification and Theorem Prover Lab: z3 theorem prover |
Z3 Constraints |
Lab-Exercise-2 |
|
| 5 |
Lecture: Code Verification Using Symbolic Execution Lab: Manual Assertion-based Verification using Z3 |
SVF Z3 APIs |
|
Assignment-2 |
| 6 |
Study Break |
|
|
|
| 7 |
Lecture: Code Verification using Symbolic Execution Lab: Automated Code Assertion Verification using Z3 |
|
|
|
| 8 |
Lecture: Abstract Interpretation Foundations Lab: Basic Concepts and Examples |
|
Lab-Exercise-3 |
Assignment-3 |
| 9 |
Lecture: Abstract Interpretation for Code Analysis and Verification Lab: Manual Abstract Interpretation |
SVF AE APIs |
|
|
| 10 |
Lecture: Buffer Overflow Detection using Abstract Interpretation Lab: Implementation and testing |
|
|
|