Automated Program Verification

Lecture 1 - Course Overview

Lecture 2 - Propositional Logic (PL)

Lecture 3 - Satisfiability and Validity in Propositional Logic

Lecture 4 - Davis-Putnam-Logemann-Loveland Algorithm (DPLL) - Part A

Lecture 5 - Davis-Putnam-Logemann-Loveland Algorithm (DPLL) - Part B

Lecture 6 - Encoding Problems in Propositional Logic

Lecture 7 - First-Order Logic (FOL)

Lecture 8 - Satisfiability and Validity in First-Order Logic - Part A

Lecture 9 - Satisfiability and Validity in First-Order Logic - Part B

Lecture 10 - Satisfiability Modulo Theories (SMT)

Lecture 11 - Theory of Equality (T_=) - Part A

Lecture 12 - Theory of Equality (T_=) - Part B

Lecture 13 - Theory of Numbers

Lecture 14 - Theory of Arrays

Lecture 15 - Combination of Theories

Lecture 16 - Compactness of FOL

Lecture 17 - Application of SMT: Bounded Model Checking

Lecture 18 - Z3 Tool

Lecture 19 - Introduction to Program Verification

Lecture 20 - Formal Definition of Program Verification

Lecture 21 - Different Forms of Program Specifications

Lecture 22 - Towards Automated Verification

Lecture 23 - Strongest Post Condition - Part A : Primitive Statements

Lecture 24 - Strongest Post Condition - Part B : Primitive Statements

Lecture 25 - Strongest Post Condition - Part C : Compound Statements

Lecture 26 - Strongest Post-Condition - Part D : Putting it all together

Lecture 27 - Soundness and Completeness of Strongest Post-Condition

Lecture 28 - Weakest Pre-condition - Part A : Primitive Statements

Lecture 29 - Weakest Pre-condition - Part B : Primitive Statements

Lecture 30 - Weakest Pre-condition - Part C : Compound Statements

Lecture 31 - Weakest Pre-condition - Part D : Putting it all together

Lecture 32 - Hoare Logic - Part A : Introduction

Lecture 33 - Hoare Logic - Part B : Inference Rules for Compound Statements

Lecture 34 - Hoare Logic - Part C : Loop Invariants

Lecture 35 - Hoare Logic - Part D : Putting it all together

Lecture 36 - Crafting Inductive Loop Invariants

Lecture 37 - Verification Condition Generation - Part A

Lecture 38 - Verification Condition Generation - Part B

Lecture 39 - Handling functions

Lecture 40 - Handling Pointers

Lecture 41 - Introduction to Abstract Interpretation

Lecture 42 - Forward Propagate Algorithm

Lecture 43 - Overview of Abstract Interpretation

Lecture 44 - Soundness of Abstract Interpretation

Lecture 45 - Lattice Theory Basics - Part A

Lecture 46 - Lattice Theory Basics - Part B

Lecture 47 - Fixpoints

Lecture 48 - Chains

Lecture 49 - Galois Connection

Lecture 50 - Concrete and Abstract Join Over Path

Lecture 51 - Defining Soundness of Abstract Interpretation

Lecture 52 - Proof of Soundness of Abstract Interpretation

Lecture 53 - Introduction to Kildall's Algorithm

Lecture 54 - Properties of Kildall's Algorithm

Lecture 55 - Kildall's Algorithm with Monotonic Transfer Functions

Lecture 56 - Kildall's Algorithm with Distributive Transfer Functions

Lecture 57 - Proof of Soundness of Kildall's Algorithm

Lecture 58 - Proof of Termination of Kildall's Algorithm

Lecture 59 - Constant Abstract Domain

Lecture 60 - Interval Abstract Domain: Introduction

Lecture 61 - Interval Abstract Domain: Widening and Narrowing

Lecture 62 - Relational Domains and Inter-Procedural Abstract Interpretation

Lecture 63 - Concrete and Symbolic Model Checking

Lecture 64 - Abstract Model Checking

Lecture 65 - Abstract Model Cheking with Cartesian Predicate Abstraction

Lecture 66 - Abstraction Refinement using Interpolation

Lecture 67 - CEGAR

Lecture 68 - Summary