Learn · Automated Program Verification

Lecture 36 of 68week-07

Crafting Inductive Loop Invariants

Prof. Kartik Nagar · IIT Madras

Credits and licence

From
Automated Program Verification, IIT Madras (at NPTEL)
Licence
CC BY-NC-SA, as NPTEL states it. Non-commercial use only.
Attribution
NPTEL states: "Distributed under Creative Commons Attribution-ShareAlike / CC BY - NC - SA", beside a BY-NC-SA badge.
Who can watch
Tweens profiles and older. How courses are placed

All the lectures

  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
  6. Encoding Problems in Propositional Logic Video
  7. First-Order Logic (FOL) Video
  8. Satisfiability and Validity in First-Order Logic Part A Video
  9. Satisfiability and Validity in First-Order Logic Part B Video
  10. Satisfiability Modulo Theories (SMT) Video
  11. Theory of Equality (T_=) Part A Video
  12. Theory of Equality (T_=) Part B Video
  13. Theory of Numbers Video
  14. Theory of Arrays Video
  15. Combination of Theories Video
  16. Compactness of FOL Video
  17. Application of SMT: Bounded Model Checking Video
  18. Z3 Tool Video
  19. Introduction to Program Verification Video
  20. Formal Definition of Program Verification Video
  21. Different Forms of Program Specifications Video
  22. Towards Automated Verification Video
  23. Strongest Post Condition Part A: Primitive Statements Video
  24. Strongest Post Condition Part B: Primitive Statements Video
  25. Strongest Post Condition Part C: Compound Statements Video
  26. Strongest Post-Condition Part D: Putting it all together Video
  27. Soundness and Completeness of Strongest Post-Condition Video
  28. Weakest Pre-condition Part A: Primitive Statements Video
  29. Weakest Pre-condition Part B: Primitive Statements Video
  30. Weakest Pre-condition Part C: Compound Statements Video
  31. Weakest Pre-condition Part D: Putting it all together Video
  32. Hoare Logic Part A: Introduction Video
  33. Hoare Logic Part B: Inference Rules for Compound Statements Video
  34. Hoare Logic Part C: Loop Invariants Video
  35. Hoare Logic Part D: Putting it all together Video
  36. Crafting Inductive Loop Invariants Video
  37. Verification Condition Generation Part A Video
  38. Verification Condition Generation Part B Video
  39. Handling functions Video
  40. Handling Pointers Video
  41. Introduction to Abstract Interpretation Video
  42. Forward Propagate Algorithm Video
  43. Overview of Abstract Interpretation Video
  44. Soundness of Abstract Interpretation Video
  45. Lattice Theory Basics Part A Video
  46. Lattice Theory Basics Part B Video
  47. Fixpoints Video
  48. Chains Video
  49. Galois Connection Video
  50. Concrete and Abstract Join Over Path Video
  51. Defining Soundness of Abstract Interpretation Video
  52. Proof of Soundness of Abstract Interpretation Video
  53. Introduction to Kildall's Algorithm Video
  54. Properties of Kildall's Algorithm Video
  55. Kildall's Algorithm with Monotonic Transfer Functions Video
  56. Kildall's Algorithm with Distributive Transfer Functions Video
  57. Proof of Soundness of Kildall's Algorithm Video
  58. Proof of Termination of Kildall's Algorithm Video
  59. Constant Abstract Domain Video
  60. Interval Abstract Domain: Introduction Video
  61. Interval Abstract Domain: Widening and Narrowing Video
  62. Relational Domains and Inter-Procedural Abstract Interpretation Video
  63. Concrete and Symbolic Model Checking Video
  64. Abstract Model Checking Video
  65. Abstract Model Cheking with Cartesian Predicate Abstraction Video
  66. Abstraction Refinement using Interpolation Video
  67. CEGAR Video
  68. Summary Video