Learn · Automated Program Verification
Lecture 33 of 68week-07
Hoare Logic Part B: Inference Rules for Compound Statements
Prof. Kartik Nagar · IIT Madras
Credits and licence
- From
- Automated Program Verification, IIT Madras (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
- Course Overview
- Propositional Logic (PL)
- Satisfiability and Validity in Propositional Logic
- Davis-Putnam-Logemann-Loveland Algorithm (DPLL) Part A
- Davis-Putnam-Logemann-Loveland Algorithm (DPLL) Part B
- Encoding Problems in Propositional Logic
- First-Order Logic (FOL)
- Satisfiability and Validity in First-Order Logic Part A
- Satisfiability and Validity in First-Order Logic Part B
- Satisfiability Modulo Theories (SMT)
- Theory of Equality (T_=) Part A
- Theory of Equality (T_=) Part B
- Theory of Numbers
- Theory of Arrays
- Combination of Theories
- Compactness of FOL
- Application of SMT: Bounded Model Checking
- Z3 Tool
- Introduction to Program Verification
- Formal Definition of Program Verification
- Different Forms of Program Specifications
- Towards Automated Verification
- Strongest Post Condition Part A: Primitive Statements
- Strongest Post Condition Part B: Primitive Statements
- Strongest Post Condition Part C: Compound Statements
- Strongest Post-Condition Part D: Putting it all together
- Soundness and Completeness of Strongest Post-Condition
- Weakest Pre-condition Part A: Primitive Statements
- Weakest Pre-condition Part B: Primitive Statements
- Weakest Pre-condition Part C: Compound Statements
- Weakest Pre-condition Part D: Putting it all together
- Hoare Logic Part A: Introduction
- Hoare Logic Part B: Inference Rules for Compound Statements
- Hoare Logic Part C: Loop Invariants
- Hoare Logic Part D: Putting it all together
- Crafting Inductive Loop Invariants
- Verification Condition Generation Part A
- Verification Condition Generation Part B
- Handling functions
- Handling Pointers
- Introduction to Abstract Interpretation
- Forward Propagate Algorithm
- Overview of Abstract Interpretation
- Soundness of Abstract Interpretation
- Lattice Theory Basics Part A
- Lattice Theory Basics Part B
- Fixpoints
- Chains
- Galois Connection
- Concrete and Abstract Join Over Path
- Defining Soundness of Abstract Interpretation
- Proof of Soundness of Abstract Interpretation
- Introduction to Kildall's Algorithm
- Properties of Kildall's Algorithm
- Kildall's Algorithm with Monotonic Transfer Functions
- Kildall's Algorithm with Distributive Transfer Functions
- Proof of Soundness of Kildall's Algorithm
- Proof of Termination of Kildall's Algorithm
- Constant Abstract Domain
- Interval Abstract Domain: Introduction
- Interval Abstract Domain: Widening and Narrowing
- Relational Domains and Inter-Procedural Abstract Interpretation
- Concrete and Symbolic Model Checking
- Abstract Model Checking
- Abstract Model Cheking with Cartesian Predicate Abstraction
- Abstraction Refinement using Interpolation
- CEGAR
- Summary