Course Information

CS 719: Topics in Mathematical Foundations of Formal Verification

Order and lattice theory:
Ordered sets: definitions, diagrammatic representations, down-sets, up-sets, maps between ordered sets

Lattices: definitions, sublattices, products, homomorphisms, ideals and filters, complete lattices, chain conditions and completeness, join-irreducible elements,

Distributive and Boolean lattices: definitions, M3−N5 theorem, Boolean lattices and Boolean algebras, results for finite distributive and finite Boolean lattices

Complete lattices, closure operators, Galois connections and completions, CPOs and fixpoint theorems

Well-quasi orders and better-quasi orders, Higman’s Lemma and applications

First-order Logic:
Quick recap of syntax, semantics, normal forms, decidability issues, completeness.

Compactness of first-order logic and its applications, Craig’s interpolation theorem, Beth’s definability theorem

Structures, isomorphism of structures, Skolem- Lowenheim theorem

Provability and refutability: Natural deduction, Gentzen’s theorem, semantic tableaux, Skolemization, refutations of universal sentences, Herbrand’s theorem, unification

Some decidable fragments of first-order logic and their decision procedures: propositional logic, equality with uninterpreted functions, linear arithmetic, Presburger logic , bit vectors, arrays, pointer logic.

Decision procedures for combinations of first-order theories: Nelson-Oppen, Shostak, Satisfiability Modulo Theories (SMT)

Type theory:
Typed lambda calculus and its extensions: dependent function spaces, Cartesian products, dependent products, disjoint union, integers, atoms, lists.

Equality and propositions as types

Subtypes and quotient types

Semantics: Computation system, type system, judgement forms

Introduction to Lattices and Orders, B. A. Davey and H. A. Priestley, Cambridge University Press, 2002
A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability and Complexity, Shawn Hedman, Oxford Texts in Logic, Oxford University, 2004
Decision Procedures: An Algorithmic Point of View, D. Kroening and O. Strichman, Springer, 2008
An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Peter B. Andrews, Springer, 2002
Types and Programming Languages, Benjamin C. Pierce, The MIT Press, 2002
Introduction to Type Theory in The Nuprl Book, Cornell University, 1995 (http://www.cs.cornell.edu/info/projects/nuprl/book/doc.html)
Articles and papers to be announced in class
Home Page

Not Available

Other Details

Duration : Full Semester Total Credit : 6
Type : Theory
Autumn Semester 2019-20

Status : Offered Instructor : Prof. Supratik Chakraborty
Spring Semester 2019-20

Status : Not Offered Instructor : ---

Last Modified Date: 15-Jul-2013


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback