Course Information
 Identification CS 719: Topics in Mathematical Foundations of Formal Verification Description 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 References 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 Prerequisites N/A 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 : ---