Home

Course Outline

#	Slides	Reading Material	Lab Exercise	Assignment
1	Lecture: Course Overview and Introduction Lab: Programming 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 Analysis Lab: 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: Automated Abstract Interpretation	SVF AE APIs
10	Lecture: Buffer Overflow Detection using Abstract Interpretation Lab: Implementation and testing