Travel; no class
Lecture by Prof. Mahesh Viswanathan: Introduction to First Order Logic
Motivations, Introduction, Course Overview, and Administrivia
Verification using Invariants
While programs, induction, invariants, inductive invariants. invariant vs reachable states, key properties of inductive invariants, , need for logic.
Verification using Dafny
Proving simple while programs using Dafny, requires/ensures clauses, invariants, arrays and quantified assertions and invariants.
Proving Termination
Proving termination using ranking functions, well-founded orders, lex ordering on pairs of naturals, ordinals.
First Order Theories
Recap of syntax and semantics of FOL, Theories, Theory of a model, Theories defined by axioms, Complete Theories.
First Order Theories
Complete and consistent theories, decidability, Godel's strong completeness theorem, Godel's incompleteness theorem,
First Order Logic
Syntax, semantics, models, interpretations, decidability, proof systems, axiom systems, Godel's completeness theorem, strong completeness, compactness, first-order theories, quantifier-free theories,decidable theories, Nelson-Oppen combination, SMT, SMT solvers
Program Verification Mechanics
Reduction of program verification to logic;
Three programs: Linear Search, Binary Search, Bubble
Sort exhibiting loops, nested loops and recursion;
Basic paths; weakest precondition; verification conditions; termination using ranking functions to well-founded orderings;
A decidable theory of arrays
Hoare Logic: proof system
while programs; Hoare logic proof system, an example proof