Learn · Formal Methods for System Verification
Lecture 45 of 56Week 10: Equivalence Checking
Equivalence Checking with SMT Solvers
Prof. Chandan Karfa · IIT Guwahati
Credits and licence
- From
- Formal Methods for System Verification, IIT Guwahati (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
- Formal Methods for System Verification: Course Introduction
- Formal Methods with Examples
- Spectrum of Logic
- Propositional Logic
- Decision Problems of Propositional Logic
- Normal Forms
- Tseitin Transformation
- Introduction to SAT Solver
- DPLL based SAT Solver
- Analyze Conflict in DPLL based method
- Overall DPLL Algorithm
- Decision Heuristics in DPLL based SAT Solver
- Preprocessing of SAT Formula
- SAT Encoding Example - Logic Locking
- SAT Tool Demo
- Binary Decision Diagrams (BDDs)
- ROBDD Construction directly from Boolean Formula
- Variable Ordering in ROBDDs
- Introduction to Formal Property Verification
- Correctness, Consistencies and Completenss of Formal Properties
- Introduction to Model Checking
- LTL: Syntax and Semantics
- LTL Encoding Examples
- LTL Equivalence of Formulas, Adequate Set, Encoding Examples
- CTL Introduction
- CTL: Syntax and Semantics
- CTL Encoding Exmaples
- CTL Model Checking Algorithm - Fixed point Concepts
- CTL Model Checking Algorithm
- Correctness of CTL Model Checking Algorithmson
- Introduction to LTL Model Checking
- Büchi Automata
- Generalized Nondeterministic B¨uchi Automata (GNBA)
- GNBA Construction from LTL Formula - States
- GNBA Construction from LTL Formula - Transitions
- BDD based Symbolic Model Checking - ROBDD Construction
- ROBDD based State Traversal in Symbolic Model Checking
- Backward Reachability in BDD based Symbolic Model Checking
- SAT based Symbolic Model Checking
- Bounded Model Checking
- Tutorial on NuSMV Model Checking Tool
- Equivalence Checking Problems in Embedded Systems
- Equivalence Checking between Programs
- Translation Validation of Loop Invariant Code Optimizations
- Equivalence Checking with SMT Solvers
- Translation Validation of Array Intensive Programs
- Verification of Sequential to Concurrent Code Transformations
- C to RTL Equivalence Checking
- RTL to C Reverse Engineering
- Combinational Equivalence Checking
- Sequential Equivalence Checking
- LLM Assisted Assertion Generation for Verification
- LLM Assisted SVA generation with Montecarlo Tree Search
- Quality of LLM Assisted SVA Generation
- Challenges and Future Directions in LLM Assisted SVA Generation
- AI Assisted Formal Verification