# Formal Methods for System Verification

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

Formal Verification is an essential tool for any Software and Hardware Industries. The industries spent more than 50% of the design cycle in verifying the functional correctness of the developed software/hardware. The techniques like Satisfiability (SAT) and model checking is the heart of those formal verification techniques used by the Industries. In this course, we will cover the fundamental theories of SAT and Model checking and take few case studies to explain its applications.

Intended audience: BTech 3rd year and final year students in CSE and Related subjects. MTech/PhD students in CSE. Industry Professionals

## Lectures

1. [Formal Methods for System Verification: Course Introduction](https://invisiblenetwork.ai/learn/nptel/106103002/28afcd57ed61) (YouTube)
2. [Formal Methods with Examples](https://invisiblenetwork.ai/learn/nptel/106103002/644cc0b8cf5a) (YouTube)
3. [Spectrum of Logic](https://invisiblenetwork.ai/learn/nptel/106103002/c36cab222ce5) (YouTube)
4. [Propositional Logic](https://invisiblenetwork.ai/learn/nptel/106103002/8ea5877b417b) (YouTube)
5. [Decision Problems of Propositional Logic](https://invisiblenetwork.ai/learn/nptel/106103002/531555b9631d) (YouTube)
6. [Normal Forms](https://invisiblenetwork.ai/learn/nptel/106103002/d4bc170f2b4e) (YouTube)
7. [Tseitin Transformation](https://invisiblenetwork.ai/learn/nptel/106103002/682bfa9ec1a0) (YouTube)
8. [Introduction to SAT Solver](https://invisiblenetwork.ai/learn/nptel/106103002/e3de3c5b33f1) (YouTube)
9. [DPLL based SAT Solver](https://invisiblenetwork.ai/learn/nptel/106103002/2f4eb204544c) (YouTube)
10. [Analyze Conflict in DPLL based method](https://invisiblenetwork.ai/learn/nptel/106103002/ae5bdcba3d7f) (YouTube)
11. [Overall DPLL Algorithm](https://invisiblenetwork.ai/learn/nptel/106103002/9e81ed09df1a) (YouTube)
12. [Decision Heuristics in DPLL based SAT Solver](https://invisiblenetwork.ai/learn/nptel/106103002/9b8c70f159c3) (YouTube)
13. [Preprocessing of SAT Formula](https://invisiblenetwork.ai/learn/nptel/106103002/42a6596ee68c) (YouTube)
14. [SAT Encoding Example - Logic Locking](https://invisiblenetwork.ai/learn/nptel/106103002/fa5e35d40467) (YouTube)
15. [SAT Tool Demo](https://invisiblenetwork.ai/learn/nptel/106103002/f72cd7fa7a5f) (YouTube)
16. [Binary Decision Diagrams (BDDs)](https://invisiblenetwork.ai/learn/nptel/106103002/914f0c1d707d) (YouTube)
17. [ROBDD Construction directly from Boolean Formula](https://invisiblenetwork.ai/learn/nptel/106103002/567b354c03f9) (YouTube)
18. [Variable Ordering in ROBDDs](https://invisiblenetwork.ai/learn/nptel/106103002/82c06eed8dd3) (YouTube)
19. [Introduction to Formal Property Verification](https://invisiblenetwork.ai/learn/nptel/106103002/d9ae15d2e133) (YouTube)
20. [Correctness, Consistencies and Completenss of Formal Properties](https://invisiblenetwork.ai/learn/nptel/106103002/803c842b7f88) (YouTube)
21. [Introduction to Model Checking](https://invisiblenetwork.ai/learn/nptel/106103002/d9201875236c) (YouTube)
22. [LTL: Syntax and Semantics](https://invisiblenetwork.ai/learn/nptel/106103002/3f837771a3e4) (YouTube)
23. [LTL Encoding Examples](https://invisiblenetwork.ai/learn/nptel/106103002/ed21b41f5427) (YouTube)
24. [LTL Equivalence of Formulas, Adequate Set, Encoding Examples](https://invisiblenetwork.ai/learn/nptel/106103002/0562e96e73a6) (YouTube)
25. [CTL Introduction](https://invisiblenetwork.ai/learn/nptel/106103002/84dacd4b6233) (YouTube)
26. [CTL: Syntax and Semantics](https://invisiblenetwork.ai/learn/nptel/106103002/fb206f44488a) (YouTube)
27. [CTL Encoding Exmaples](https://invisiblenetwork.ai/learn/nptel/106103002/56778177142c) (YouTube)
28. [CTL Model Checking Algorithm - Fixed point Concepts](https://invisiblenetwork.ai/learn/nptel/106103002/c4ffbb0599a0) (YouTube)
29. [CTL Model Checking Algorithm](https://invisiblenetwork.ai/learn/nptel/106103002/5bb032f5c101) (YouTube)
30. [Correctness of CTL Model Checking Algorithmson](https://invisiblenetwork.ai/learn/nptel/106103002/c48f514f8e03) (YouTube)
31. [Introduction to LTL Model Checking](https://invisiblenetwork.ai/learn/nptel/106103002/559c9a96fb2f) (YouTube)
32. [Büchi Automata](https://invisiblenetwork.ai/learn/nptel/106103002/952de6522b88) (YouTube)
33. [Generalized Nondeterministic B¨uchi Automata (GNBA)](https://invisiblenetwork.ai/learn/nptel/106103002/62d52f7fa1c4) (YouTube)
34. [GNBA Construction from LTL Formula - States](https://invisiblenetwork.ai/learn/nptel/106103002/70e2f1fb2075) (YouTube)
35. [GNBA Construction from LTL Formula - Transitions](https://invisiblenetwork.ai/learn/nptel/106103002/cd1fe7028e52) (YouTube)
36. [BDD based Symbolic Model Checking - ROBDD Construction](https://invisiblenetwork.ai/learn/nptel/106103002/20b0cd8618c8) (YouTube)
37. [ROBDD based State Traversal in Symbolic Model Checking](https://invisiblenetwork.ai/learn/nptel/106103002/154630a20f91) (YouTube)
38. [Backward Reachability in BDD based Symbolic Model Checking](https://invisiblenetwork.ai/learn/nptel/106103002/22b79bd95a05) (YouTube)
39. [SAT based Symbolic Model Checking](https://invisiblenetwork.ai/learn/nptel/106103002/fbdb847f8ea7) (YouTube)
40. [Bounded Model Checking](https://invisiblenetwork.ai/learn/nptel/106103002/2d5ef7458cc0) (YouTube)
41. [Tutorial on NuSMV Model Checking Tool](https://invisiblenetwork.ai/learn/nptel/106103002/7c4eb1ad9027) (YouTube)
42. [Equivalence Checking Problems in Embedded Systems](https://invisiblenetwork.ai/learn/nptel/106103002/3a9f94d00c01) (YouTube)
43. [Equivalence Checking between Programs](https://invisiblenetwork.ai/learn/nptel/106103002/a4ad5781443c) (YouTube)
44. [Translation Validation of Loop Invariant Code Optimizations](https://invisiblenetwork.ai/learn/nptel/106103002/77611211b370) (YouTube)
45. [Equivalence Checking with SMT Solvers](https://invisiblenetwork.ai/learn/nptel/106103002/60eac7396e94) (YouTube)
46. [Translation Validation of Array Intensive Programs](https://invisiblenetwork.ai/learn/nptel/106103002/f15f4241d53b) (YouTube)
47. [Verification of Sequential to Concurrent Code Transformations](https://invisiblenetwork.ai/learn/nptel/106103002/569d8cdd2b0b) (YouTube)
48. [C to RTL Equivalence Checking](https://invisiblenetwork.ai/learn/nptel/106103002/2384bf7df51f) (YouTube)
49. [RTL to C Reverse Engineering](https://invisiblenetwork.ai/learn/nptel/106103002/ea232196a4bf) (YouTube)
50. [Combinational Equivalence Checking](https://invisiblenetwork.ai/learn/nptel/106103002/da1e25a709cd) (YouTube)
51. [Sequential Equivalence Checking](https://invisiblenetwork.ai/learn/nptel/106103002/ed594a2d663b) (YouTube)
52. [LLM Assisted Assertion Generation for Verification](https://invisiblenetwork.ai/learn/nptel/106103002/a1f9beb5b8c9) (YouTube)
53. [LLM Assisted SVA generation with Montecarlo Tree Search](https://invisiblenetwork.ai/learn/nptel/106103002/53629fd6627d) (YouTube)
54. [Quality of LLM Assisted SVA Generation](https://invisiblenetwork.ai/learn/nptel/106103002/6a9059d348b1) (YouTube)
55. [Challenges and Future Directions in LLM Assisted SVA Generation](https://invisiblenetwork.ai/learn/nptel/106103002/92b2c5f709c7) (YouTube)
56. [AI Assisted Formal Verification](https://invisiblenetwork.ai/learn/nptel/106103002/dc46412fef81) (YouTube)