# Automated Program Verification

- Institution: IIT Madras
- Department: Computer Science and Engineering
- Teacher: Prof. Kartik Nagar
- Level: Undergraduate
- Language: English
- Subjects: Computer science, Engineering
- Source: [NPTEL](https://nptel.ac.in/courses/106106714)
- Licence: [CC BY-NC-SA](https://nptel.ac.in/faq) (Non-commercial use only.)
- Syllabus: [at the source](https://nptel.ac.in/courses/106106714)
- Who can watch: Tweens profiles and older (sources give no ratings; placed by Invisible Network from the source's own words)

## Lectures

1. [Course Overview](https://invisiblenetwork.ai/learn/nptel/106106714/88fa4ad57933) (Video)
2. [Propositional Logic (PL)](https://invisiblenetwork.ai/learn/nptel/106106714/5fd65a3f718d) (Video)
3. [Satisfiability and Validity in Propositional Logic](https://invisiblenetwork.ai/learn/nptel/106106714/778fa1ac9f51) (Video)
4. [Davis-Putnam-Logemann-Loveland Algorithm (DPLL) Part A](https://invisiblenetwork.ai/learn/nptel/106106714/75f4ee9cb449) (Video)
5. [Davis-Putnam-Logemann-Loveland Algorithm (DPLL) Part B](https://invisiblenetwork.ai/learn/nptel/106106714/d0a7b4112e8f) (Video)
6. [Encoding Problems in Propositional Logic](https://invisiblenetwork.ai/learn/nptel/106106714/0a17b2fe7d34) (Video)
7. [First-Order Logic (FOL)](https://invisiblenetwork.ai/learn/nptel/106106714/ba7474c9bc37) (Video)
8. [Satisfiability and Validity in First-Order Logic Part A](https://invisiblenetwork.ai/learn/nptel/106106714/83663cabcdaf) (Video)
9. [Satisfiability and Validity in First-Order Logic Part B](https://invisiblenetwork.ai/learn/nptel/106106714/3b8bec46035e) (Video)
10. [Satisfiability Modulo Theories (SMT)](https://invisiblenetwork.ai/learn/nptel/106106714/55a52c498d7c) (Video)
11. [Theory of Equality (T_=) Part A](https://invisiblenetwork.ai/learn/nptel/106106714/890b25d0d881) (Video)
12. [Theory of Equality (T_=) Part B](https://invisiblenetwork.ai/learn/nptel/106106714/25c04a9bf8b1) (Video)
13. [Theory of Numbers](https://invisiblenetwork.ai/learn/nptel/106106714/96b5b540926c) (Video)
14. [Theory of Arrays](https://invisiblenetwork.ai/learn/nptel/106106714/6aed54035a25) (Video)
15. [Combination of Theories](https://invisiblenetwork.ai/learn/nptel/106106714/2e1866a26702) (Video)
16. [Compactness of FOL](https://invisiblenetwork.ai/learn/nptel/106106714/b3e0b690e382) (Video)
17. [Application of SMT: Bounded Model Checking](https://invisiblenetwork.ai/learn/nptel/106106714/abb58e41ae54) (Video)
18. [Z3 Tool](https://invisiblenetwork.ai/learn/nptel/106106714/9004e5537478) (Video)
19. [Introduction to Program Verification](https://invisiblenetwork.ai/learn/nptel/106106714/4b3120cf821a) (Video)
20. [Formal Definition of Program Verification](https://invisiblenetwork.ai/learn/nptel/106106714/b66b75295b1a) (Video)
21. [Different Forms of Program Specifications](https://invisiblenetwork.ai/learn/nptel/106106714/844fbdaec69b) (Video)
22. [Towards Automated Verification](https://invisiblenetwork.ai/learn/nptel/106106714/e96de2a5dd22) (Video)
23. [Strongest Post Condition Part A: Primitive Statements](https://invisiblenetwork.ai/learn/nptel/106106714/751cc0cc8a07) (Video)
24. [Strongest Post Condition Part B: Primitive Statements](https://invisiblenetwork.ai/learn/nptel/106106714/633f11bce619) (Video)
25. [Strongest Post Condition Part C: Compound Statements](https://invisiblenetwork.ai/learn/nptel/106106714/1bafb848b25d) (Video)
26. [Strongest Post-Condition Part D: Putting it all together](https://invisiblenetwork.ai/learn/nptel/106106714/0e021992a892) (Video)
27. [Soundness and Completeness of Strongest Post-Condition](https://invisiblenetwork.ai/learn/nptel/106106714/a006975b82c2) (Video)
28. [Weakest Pre-condition Part A: Primitive Statements](https://invisiblenetwork.ai/learn/nptel/106106714/653936722339) (Video)
29. [Weakest Pre-condition Part B: Primitive Statements](https://invisiblenetwork.ai/learn/nptel/106106714/a9c60f7f0641) (Video)
30. [Weakest Pre-condition Part C: Compound Statements](https://invisiblenetwork.ai/learn/nptel/106106714/249a7a8b7b77) (Video)
31. [Weakest Pre-condition Part D: Putting it all together](https://invisiblenetwork.ai/learn/nptel/106106714/ae1480711b27) (Video)
32. [Hoare Logic Part A: Introduction](https://invisiblenetwork.ai/learn/nptel/106106714/daa6ffc4cbc2) (Video)
33. [Hoare Logic Part B: Inference Rules for Compound Statements](https://invisiblenetwork.ai/learn/nptel/106106714/1f85afee466f) (Video)
34. [Hoare Logic Part C: Loop Invariants](https://invisiblenetwork.ai/learn/nptel/106106714/7a962ef8462a) (Video)
35. [Hoare Logic Part D: Putting it all together](https://invisiblenetwork.ai/learn/nptel/106106714/014a67fe4e12) (Video)
36. [Crafting Inductive Loop Invariants](https://invisiblenetwork.ai/learn/nptel/106106714/838196dca8a6) (Video)
37. [Verification Condition Generation Part A](https://invisiblenetwork.ai/learn/nptel/106106714/676c6acd8eaa) (Video)
38. [Verification Condition Generation Part B](https://invisiblenetwork.ai/learn/nptel/106106714/19d57e1494df) (Video)
39. [Handling functions](https://invisiblenetwork.ai/learn/nptel/106106714/7df9cff4310a) (Video)
40. [Handling Pointers](https://invisiblenetwork.ai/learn/nptel/106106714/2b5dc7bf8746) (Video)
41. [Introduction to Abstract Interpretation](https://invisiblenetwork.ai/learn/nptel/106106714/71707060302c) (Video)
42. [Forward Propagate Algorithm](https://invisiblenetwork.ai/learn/nptel/106106714/f4e4feaf8d8d) (Video)
43. [Overview of Abstract Interpretation](https://invisiblenetwork.ai/learn/nptel/106106714/85d8952e1f65) (Video)
44. [Soundness of Abstract Interpretation](https://invisiblenetwork.ai/learn/nptel/106106714/cd8a78cef1bf) (Video)
45. [Lattice Theory Basics Part A](https://invisiblenetwork.ai/learn/nptel/106106714/2eece85d94a6) (Video)
46. [Lattice Theory Basics Part B](https://invisiblenetwork.ai/learn/nptel/106106714/36e84a8dfcac) (Video)
47. [Fixpoints](https://invisiblenetwork.ai/learn/nptel/106106714/6c3e6678c7ec) (Video)
48. [Chains](https://invisiblenetwork.ai/learn/nptel/106106714/49c5d87e89cc) (Video)
49. [Galois Connection](https://invisiblenetwork.ai/learn/nptel/106106714/8b1bcd238ab9) (Video)
50. [Concrete and Abstract Join Over Path](https://invisiblenetwork.ai/learn/nptel/106106714/c9da93e595e3) (Video)
51. [Defining Soundness of Abstract Interpretation](https://invisiblenetwork.ai/learn/nptel/106106714/4ca8e54a1983) (Video)
52. [Proof of Soundness of Abstract Interpretation](https://invisiblenetwork.ai/learn/nptel/106106714/79e8d4dd1d75) (Video)
53. [Introduction to Kildall's Algorithm](https://invisiblenetwork.ai/learn/nptel/106106714/3df5e14237c7) (Video)
54. [Properties of Kildall's Algorithm](https://invisiblenetwork.ai/learn/nptel/106106714/60990c1e740f) (Video)
55. [Kildall's Algorithm with Monotonic Transfer Functions](https://invisiblenetwork.ai/learn/nptel/106106714/764287dc7486) (Video)
56. [Kildall's Algorithm with Distributive Transfer Functions](https://invisiblenetwork.ai/learn/nptel/106106714/5bfecdcd2622) (Video)
57. [Proof of Soundness of Kildall's Algorithm](https://invisiblenetwork.ai/learn/nptel/106106714/386abd099eb4) (Video)
58. [Proof of Termination of Kildall's Algorithm](https://invisiblenetwork.ai/learn/nptel/106106714/b0c2d9d9365c) (Video)
59. [Constant Abstract Domain](https://invisiblenetwork.ai/learn/nptel/106106714/4ad917d9aee2) (Video)
60. [Interval Abstract Domain: Introduction](https://invisiblenetwork.ai/learn/nptel/106106714/de199749201a) (Video)
61. [Interval Abstract Domain: Widening and Narrowing](https://invisiblenetwork.ai/learn/nptel/106106714/31e36a103fb3) (Video)
62. [Relational Domains and Inter-Procedural Abstract Interpretation](https://invisiblenetwork.ai/learn/nptel/106106714/57f097f619bb) (Video)
63. [Concrete and Symbolic Model Checking](https://invisiblenetwork.ai/learn/nptel/106106714/cb4417ce0705) (Video)
64. [Abstract Model Checking](https://invisiblenetwork.ai/learn/nptel/106106714/76a15126d76e) (Video)
65. [Abstract Model Cheking with Cartesian Predicate Abstraction](https://invisiblenetwork.ai/learn/nptel/106106714/781d734f319f) (Video)
66. [Abstraction Refinement using Interpolation](https://invisiblenetwork.ai/learn/nptel/106106714/7b380c3036cc) (Video)
67. [CEGAR](https://invisiblenetwork.ai/learn/nptel/106106714/5b53873990f4) (Video)
68. [Summary](https://invisiblenetwork.ai/learn/nptel/106106714/22ab4d41d28d) (Video)