NPTEL Course: Formal Methods for System Verification

Course Outline

Week 1

• Course Introduction
• Formal Verification with Example: Introduction to Model Checking and Theorem Proving
• Spectrum of Logic with Examples

Week 2

• Proposition Logic: Syntax, Semantic, Axioms
• Decidability of Propositional Logic
• Introduction to First Order Logic
• First Order Logic: Syntax, Semantic and examples

Week 3

• First order logic - Axioms, Decidability of First order logic
• Higher Order Logic
• Normal Forms: NNF, CNF, DNF, Conversion to normal Forms
• Tsetin Transformations

Week 4

• SAT Solving: Introduction Conflict Clause, Backtrack, Analyze clause
• SAT Solving: Introduction SAT Solvers
• SAT Solving: Implication Graph, Backtrack, CDCL
• SAT Solving: DPLL Algorithm

Week 5

• SAT Solving: Analyze Conflict, UIP, Conflict Clause heuristics
• SAT Solving: Decision Heuristics, DIMACS format
• SAT Solving: Preprocessing of SAT formula
• Case Study on SAT based modeling

Week 6

• BDD, ROBDD, Reduction Rules
• Direct ROBDD construction
• Variable Ordering in BDD

Week 7

• Formal Property verification (FPV)
• Introduction to Model Checking
• FPV with Examples
• Correctness, Consistency and Completeness of FPV

Week 8

• LTL - Syntax and Semantic
• LTL Encoding examples
• CTL: Syntax and Semantic
• CTL Encoding examples

Week 9

• CTL Model Checking Algorithm
• CTL Model Checking Algorithm
• Correctness of CTL Model Checking Algorithm

Week 10

• LTL Model Checking, Buchi Automata, NBA, GNBA
• LTL to GNBA Construction
• LTL Model Checking Algorithm

Week 11

• Symbolic Model Checking with BDD
• Symbolic Model Checking with BDD
• SAT based Symbolic Model Checking
• SAT based Symbolic Model Checking

Week 12

• Bounded Model Checking
• Case Study1: Formal Verification in Hardware Design
• Case Study2: Formal Verification in Hardware Design
• Case Study3: Formal Verification in Hardware Design