Learn · NPTEL

Course10610671468 lectures

Automated Program Verification

Prof. Kartik Nagar · IIT Madras

Start with lecture 1 At NPTEL

Lectures

week-01

  1. Course Overview Video
  2. Propositional Logic (PL) Video
  3. Satisfiability and Validity in Propositional Logic Video
  4. Davis-Putnam-Logemann-Loveland Algorithm (DPLL) Part A Video
  5. Davis-Putnam-Logemann-Loveland Algorithm (DPLL) Part B Video

week-02

  1. Encoding Problems in Propositional Logic Video
  2. First-Order Logic (FOL) Video
  3. Satisfiability and Validity in First-Order Logic Part A Video
  4. Satisfiability and Validity in First-Order Logic Part B Video
  5. Satisfiability Modulo Theories (SMT) Video

week-03

  1. Theory of Equality (T_=) Part A Video
  2. Theory of Equality (T_=) Part B Video
  3. Theory of Numbers Video
  4. Theory of Arrays Video
  5. Combination of Theories Video

week-04

  1. Compactness of FOL Video
  2. Application of SMT: Bounded Model Checking Video
  3. Z3 Tool Video
  4. Introduction to Program Verification Video
  5. Formal Definition of Program Verification Video
  6. Different Forms of Program Specifications Video

week-05

  1. Towards Automated Verification Video
  2. Strongest Post Condition Part A: Primitive Statements Video
  3. Strongest Post Condition Part B: Primitive Statements Video
  4. Strongest Post Condition Part C: Compound Statements Video
  5. Strongest Post-Condition Part D: Putting it all together Video

week-06

  1. Soundness and Completeness of Strongest Post-Condition Video
  2. Weakest Pre-condition Part A: Primitive Statements Video
  3. Weakest Pre-condition Part B: Primitive Statements Video
  4. Weakest Pre-condition Part C: Compound Statements Video
  5. Weakest Pre-condition Part D: Putting it all together Video

week-07

  1. Hoare Logic Part A: Introduction Video
  2. Hoare Logic Part B: Inference Rules for Compound Statements Video
  3. Hoare Logic Part C: Loop Invariants Video
  4. Hoare Logic Part D: Putting it all together Video
  5. Crafting Inductive Loop Invariants Video
  6. Verification Condition Generation Part A Video

week-08

  1. Verification Condition Generation Part B Video
  2. Handling functions Video
  3. Handling Pointers Video
  4. Introduction to Abstract Interpretation Video
  5. Forward Propagate Algorithm Video
  6. Overview of Abstract Interpretation Video
  7. Soundness of Abstract Interpretation Video

week-09

  1. Lattice Theory Basics Part A Video
  2. Lattice Theory Basics Part B Video
  3. Fixpoints Video
  4. Chains Video
  5. Galois Connection Video

week-10

  1. Concrete and Abstract Join Over Path Video
  2. Defining Soundness of Abstract Interpretation Video
  3. Proof of Soundness of Abstract Interpretation Video
  4. Introduction to Kildall's Algorithm Video
  5. Properties of Kildall's Algorithm Video
  6. Kildall's Algorithm with Monotonic Transfer Functions Video

week-11

  1. Kildall's Algorithm with Distributive Transfer Functions Video
  2. Proof of Soundness of Kildall's Algorithm Video
  3. Proof of Termination of Kildall's Algorithm Video
  4. Constant Abstract Domain Video
  5. Interval Abstract Domain: Introduction Video
  6. Interval Abstract Domain: Widening and Narrowing Video
  7. Relational Domains and Inter-Procedural Abstract Interpretation Video

week-12

  1. Concrete and Symbolic Model Checking Video
  2. Abstract Model Checking Video
  3. Abstract Model Cheking with Cartesian Predicate Abstraction Video
  4. Abstraction Refinement using Interpolation Video
  5. CEGAR Video
  6. Summary Video

Syllabus and materials

At NPTEL, as the course publishes them.

Credits and licence

Institution
IIT Madras
Department
Computer Science and Engineering
Teacher
Prof. Kartik Nagar
Level
Undergraduate
Language
English
Subjects
Computer science, Engineering
Source
NPTEL
Licence
CC BY-NC-SA, as NPTEL states it. Non-commercial use only. NPTEL's terms
Attribution
NPTEL states: "Distributed under Creative Commons Attribution-ShareAlike / CC BY - NC - SA", beside a BY-NC-SA badge.
Who can watch
NPTEL gives no rating. Invisible Network shows it to Tweens profiles and older, judged from what the source says about it. How courses are placed