CS 477 - Formal Software Development Methods (Fall 2016)

CS 477 - Formal Software Development Methods (Fall 2016)

Lecture Schedule

Introduction and Motivation

Wed Jan 16

Travel; no class

Fri Jan 18

Lecture by Prof. Mahesh Viswanathan: Introduction to First Order Logic

Wed Jan 23 lecture notes

Motivations, Introduction, Course Overview, and Administrivia

Wed Jan 30: Arctic weather, classes cancelled
..

Program Verification Basics

Fri, Feb 1st
[lecture notes]

Verification using Invariants
While programs, induction, invariants, inductive invariants. invariant vs reachable states, key properties of inductive invariants, , need for logic.

Wed, Feb 6th
[lecture notes]

Verification using Dafny
Proving simple while programs using Dafny, requires/ensures clauses, invariants, arrays and quantified assertions and invariants.

Fri, Feb 8th
[lecture notes]

Proving Termination
Proving termination using ranking functions, well-founded orders, lex ordering on pairs of naturals, ordinals.

Logic

Wed Feb 13, 15
[lecture notes]

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,

Older lectures from a previous offering of this course

--
[lecture notes]

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

--
[lecture notes]

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

--
[lecture notes]

Hoare Logic: proof system
while programs; Hoare logic proof system, an example proof