Learn · NPTEL

Course10610300256 lectures

Formal Methods for System Verification

Prof. Chandan Karfa · IIT Guwahati

Start with lecture 1 At NPTEL

About

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

Week 1: Introduction

  1. Formal Methods for System Verification: Course Introduction YouTube
  2. Formal Methods with Examples YouTube
  3. Spectrum of Logic YouTube

Week 2: Propositional Logic

  1. Propositional Logic YouTube
  2. Decision Problems of Propositional Logic YouTube
  3. Normal Forms YouTube
  4. Tseitin Transformation YouTube

Week 3: SAT Solver

  1. Introduction to SAT Solver YouTube
  2. DPLL based SAT Solver YouTube
  3. Analyze Conflict in DPLL based method YouTube
  4. Overall DPLL Algorithm YouTube
  5. Decision Heuristics in DPLL based SAT Solver YouTube
  6. Preprocessing of SAT Formula YouTube

Week 4: Binary Decision Diagram

  1. SAT Encoding Example - Logic Locking YouTube
  2. SAT Tool Demo YouTube
  3. Binary Decision Diagrams (BDDs) YouTube
  4. ROBDD Construction directly from Boolean Formula YouTube
  5. Variable Ordering in ROBDDs YouTube

Week 5: Formal Property Verification

  1. Introduction to Formal Property Verification YouTube
  2. Correctness, Consistencies and Completenss of Formal Properties YouTube
  3. Introduction to Model Checking YouTube
  4. LTL: Syntax and Semantics YouTube
  5. LTL Encoding Examples YouTube

Week 6: LTL and CTL

  1. LTL Equivalence of Formulas, Adequate Set, Encoding Examples YouTube
  2. CTL Introduction YouTube
  3. CTL: Syntax and Semantics YouTube
  4. CTL Encoding Exmaples YouTube

Week 7: CTL and LTL Model Checking Algorithm

  1. CTL Model Checking Algorithm - Fixed point Concepts YouTube
  2. CTL Model Checking Algorithm YouTube
  3. Correctness of CTL Model Checking Algorithmson YouTube
  4. Introduction to LTL Model Checking YouTube
  5. Büchi Automata YouTube

Week 8: CTL and LTL Model Checking Algorithms

  1. Generalized Nondeterministic B¨uchi Automata (GNBA) YouTube
  2. GNBA Construction from LTL Formula - States YouTube
  3. GNBA Construction from LTL Formula - Transitions YouTube
  4. BDD based Symbolic Model Checking - ROBDD Construction YouTube
  5. ROBDD based State Traversal in Symbolic Model Checking YouTube

week 9: Symbolic Model Checking

  1. Backward Reachability in BDD based Symbolic Model Checking YouTube
  2. SAT based Symbolic Model Checking YouTube
  3. Bounded Model Checking YouTube
  4. Tutorial on NuSMV Model Checking Tool YouTube

Week 10: Equivalence Checking

  1. Equivalence Checking Problems in Embedded Systems YouTube
  2. Equivalence Checking between Programs YouTube
  3. Translation Validation of Loop Invariant Code Optimizations YouTube
  4. Equivalence Checking with SMT Solvers YouTube
  5. Translation Validation of Array Intensive Programs YouTube

Week 11

  1. Verification of Sequential to Concurrent Code Transformations YouTube
  2. C to RTL Equivalence Checking YouTube
  3. RTL to C Reverse Engineering YouTube
  4. Combinational Equivalence Checking YouTube
  5. Sequential Equivalence Checking YouTube

Week12: AI Assisted Formal Verification

  1. LLM Assisted Assertion Generation for Verification YouTube
  2. LLM Assisted SVA generation with Montecarlo Tree Search YouTube
  3. Quality of LLM Assisted SVA Generation YouTube
  4. Challenges and Future Directions in LLM Assisted SVA Generation YouTube
  5. AI Assisted Formal Verification YouTube

Syllabus and materials

At NPTEL, as the course publishes them.

Credits and licence

Institution
IIT Guwahati
Department
Computer Science and Engineering
Teacher
Prof. Chandan Karfa
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