Mod-01 Lec-38 Verification of WHILE Programs

Course Lectures

• Mod-01 Lec-01 Introduction

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-02 Propositional Logic Syntax

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-03 Semantics of Propositional Logic

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-04 Logical and Algebraic Concepts

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-05 Identities and Normal forms

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-06 Tautology Checking

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-07 Propositional Unsatisfiability

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-08 Analytic Tableaux

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-09 Consistency and Completeness

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-10 The Completeness Theorem

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-11 Maximally Consistent Sets

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-12 Formal Theories

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-13 Proof Theory : Hilbert-style

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-14 Derived Rules

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-15 The Hilbert System : Soundness

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-16 The Hilbert System :Completeness

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-17 Introduction to Predicate Logic

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-18 The Semantic of Predicate Logic

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-19 Subsitutions

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-20 Models

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-21 Structures and Substructures

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-22 First - Order Theories

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-23 Predicate Logic: Proof Theory (Contd..)

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-24 Existential Quantification

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-25 Normal Forms

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-26 Skalemization

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-27 Substitutions and Instantiations

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-28 Unification

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-29 Resolution in FOL

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-30 More on Resolution in FOL

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-31 Resolution : Soundness and Completeness

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-32 Resolution and Tableaux

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-33 Completeness of Tableaux Method

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-34 Completeness of the Hilbert System

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-35 First -Order Theories

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-36 Towards Logic Programming

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-37 Verification of Imperative Programs

  Prof. S. Arun Kumar

  Play
• Mod-01 Lec-38 Verification of WHILE Programs

  Prof. S. Arun Kumar

  Playing
• Mod-01 Lec-39 References

  Prof. S. Arun Kumar

  Play