Here is a list of topics that we plan to cover in the class.

Unit 1: Type systems

• Functional programming in Ocaml
• Type systems
• Research discussion: Types for information flow.

Unit 2: Data flow analysis and abstract interpretation

• Data flow analysis as graph reachability
• Logical abstract interpretation
• Numerical abstract domains: interval, polyhedra, and octagon domains
• Research discussion: Robustness analysis of neural networks.

Unit 3: Model Checking

• Temporal logics
• SPIN: explicit-state model checking
• Research discussion: Dynamic partial order reduction.

Unit 4: SAT and SMT solvers

• SAT-solving
• First-order logic
• Decision procedures: Theory of equality, linear arithmetic
• Research discussion: Syntax-guided synthesis.

Unit 5: Deductive verification

• Hoare logic: partial and total correctness
• Connections with abstract interpretation
• Research discussion: Separation logic in Viper.

Unit 6: Sytematic program testing 

• Bounded model checking
• Concolic testing
• Research discussion: SAGE: whitebox fuzzing.

Unit 7: Software model checking 

• The SLAM approach to software model checking 
• Research discussion: Lazy abstraction with interpolants.

Unit 8: Invariant synthesis

• Abstract interpretation (again)
• Template-based invariant generation
• Research discussion: ICE-learning.

Unit 9: Program synthesis

• Program sketching
• Example-directed synthesis: FlashMeta, Lambda2
• Research discussion: Type-directed synthesis: Synquid
• Research discussion: Neural program synthesis: Deepcoder and Bayou