CS719: Topics in Mathematical Foundations of Formal Verification
Autumn 2013


Instructor Supratik Chakraborty email: supratik [AT] cse ...
Teaching Assistant Nehul Jain email: 134050006 [AT] iitb ...

Announcements

Course Information

The purpose of this course is to provide students with a moderately in-depth exposure to a selection of mathematical topics that are needed as prerequisites for an advanced course or project in formal verification. This course is a prerequisite for CS615 "Formal Specification and Verification of Programs" to be offered in Spring 2013. The exposure provided by this course is intended to benefit students not necessarily working in the area of formal verification, but in related areas like programming languages, program analysis and optimization and logic.
This is a graduate level course recommended for students with a serious interest in formal methods and related areas. Good working knowledge of propositional logic and undergraduate level discrete mathematics is required for crediting/auditing the course.
IMPORTANT: Students are required to put in 4 to 8 hours of reading per week beyond the contact hours in class.

Hours

What When Where
Lectures Mon 14:00-15:30,
Thu 14:00-15:30
SIC 305, KReSIT building
Office hour Wed 16:30-17:30 CFDVS Lab 1 (Maths basement)
(strictly by email appointment)

Grading

Midsem 30 + x%
Endterm 50%
Quizes x% (x <= 20)

Some more logistics ...

  • All exams/quizes will be open book, notes and any material brought to the exam hall.
  • If you miss an exam for a genuine reason, meet the instructor after setting up an appointment.
  • There will be practice problems, but no graded assignments. If you attempt these practice problems sincerely, you are certain to benefit in your performance in the exams.
  • Informal discussion among students for the purpose of clarification is strongly encouraged.
  • There will be zero tolerance for dishonest means like copying solutions from others in quizzes, projects and end-term exam. Anybody found indulging in such activities will be summarily awarded an FR grade. The onus will be on the supposed offender to prove his or her innocence.
  • Problems for solving ...

    Problems from previous years' [ Aut'10 , Aut'09 , Spr'09 ] course offerings can be found on the respective course web pages.
    Practice Problem Set 1 (First-order Logic) Posted on Sep 3, 2013
    Mid-semester Exam Sep 13, 2013

    Reading Material and References

    • Shawn Hedman, A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability and Complexity , Reprinted in 2006, Oxford Texts in Logic, Oxford University Press (Text for course) .
    • Michael Huth and Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems , Second Edition, Cambridge University Press (Text for course) .
    • B. A. Davey and H. A. Priestley, Introduction to Lattices and Orders, Second edition, Cambridge University Press, 2001 (Text for course)
    • D. Kroening and O. Strichman, Decision Procedures: An Algorithmic Point of View , Springer, 2008 (Reference)
    • An excellent set of lectures notes on the Nelson-Oppen decision procedure by Prof. George Necula (Univ. of California, Berkeley)
    • An excellent tutorial introduction to Separation Logic by Peter O'Hearn. The first part of the tutorial is mostly relevant for what we have covered in class about separation logic.
    • A short introduction to Hoare Logic and the use of separation logic in proving properties of programs.
      Note that the semantics of x |-> y as given in the slides is slightly different from what we have studied in class. We will use the semantics studied in class, i.e. one that uses dom(h) = {x}, instead of dom(h) contains x

    Current Reading List

    • Chapters 1 and 2 of Logic in Computer Science:... by M. Huth and M. Ryan
    • Chapters 1, 2 and 3 of A First Course in Logic: ... by Shawn Hedman.
    • Chapters 2 and 10 of Decision Procedures: An Algorithmic Point of View by D. Kroening and O. Strichman (available in Central Library)

    Lecture Schedule

    Date Topics details
    Jul 29 Course overview and prerequisites. Syntax and semantics of first order logic (FOL), notion of structures
    Aug 1 Notion of free and bound variables in FOL, examples of interesting first-order structures: graphs, relational databases, integers; expressing properties of these structures using FOL formulae, notions of satisfiability and validity
    Aug 5 Undecidability of FOL, semantic and syntactic entailment in FOL, introduction to a proof system for FOL.
    Aug 8 A closer look at proof systems: dealing with propositional operators, soundness and completeness of proof systems, a proof of completeness theorem of propositional logic
    Aug 12 Compactness Theorem of propositional logic, and some applications in lifting results from finite structures to infinite structures
    Aug 15 Independence Day
    Aug 19 Using Compactness Theorem of propositional logic to show some inexpressibility results. Prenex normal forms and Skolem normal form in FOL. Skolemization and Skolem functions. Notion of equisatisfiability; equisatisfiability of a FOL formula and its Skolemized form.
    Aug 22 Study of Skolem normal form formulas: Herbrand universe, Herbrand interpretation of functions, Herbrand structures. Sufficiency of Herbrand structures for checking satisfiability of Skolem normal form formulas. Herbrand's unsatisfiability Theorem.
    Aug 26 More on Herbrand structures and their implications; decidability of some fragments of FOL, Compactness Theorem of FOL (in the countable case),
    Aug 29 Compactness Theorem of FOL, and applications in proving inexpressibility results in FOL.
    Sep 2 Convering FOL formulae with equality to equisatisfiable formulae without equality; illustration using examples. Using Compactness Theorem of FOL to show Completeness Theorem of FOL in a restricted setting.
    Sep 5 Decision procedures and their significance in applications. Resolution in propositional logic: resolvents, resolution algorithm, termination of the algorithm, examples
    Sep 7 Resolution in first-order logic: generalizing resolvents from those studied in propositional logic, most general unifier, algorithm for finding most general unifier of a set of literals and its proof of correctness, resolution algorithm for first order logic and its correctness.
    Sep 9, 12, 16 Mid-semester week
    Sep 13 Mid-semester exam
    Sep 23 Discussion on solutions of mid-semester exam. Introduction to Reduced Ordered Binary Decision Diagrams (ROBDDs): Shannon decomposition, if-then-else operator and DAG-based representation of propositional logic formulae.
    Sep 26 Further discussion on ROBDDs: computing the ROBDD of f op g from ROBDDs of f and g for any binary operator op. Importance of getting a good ordering of variables in ROBDDs. Introduction to Davis-Putnam-Loveland-Longemann (DPLL) algorithm for deciding CNF propositional logic formulae.
    Sep 30 Further discussion on the DPLL algorithm, backtracking and backjumping. Introduction to satisfiability modulo theories (SMT), examples of theories: arrays, lists, uninterpretted functions with equality, linear arithmetic over integers, linear arithmetic over reals.
    Oct 3 Notion of pure formulae and mixed formulae, purification of formulae in a combination of theories, using propositionalization of theory predicates and DPLL to reduce satisfiability checking of arbitrary formulae in a combination of theories to satisfiability checking of a conjunction of literals, each of which is pure.
    Oct 7 Nelson-Oppen algorithm for checking satisfiability of a conjunction of pure literals, using decision procedures of individual theories. Notion of equality propagation, soundness of Nelson-Oppen algorithm. Conditions on theories for completeness of algorithm: stably-infinite and convex theories.
    Oct 10 Proof of completeness of Nelson-Oppen algorithm for combinations of stably-infinite and convex theories. Dealing with theories that do not satisfy these requirements in practice.