CS719: Topics in Mathematical Foundations of Formal Verification
Autumn 2019

Instructor Supratik Chakraborty email: supratik [AT] cse ...


  • This offering of CS719 is different from previous offerings. Please see Course Information for more details.
  • CSE undergraduate students (BTech3 and BTech4) desirous of taking the course must meet the instructor separately within the first week of classes.
  • Please subscribe to moodle, and also to piazza for CS 719.
  • Reference material for 2-CNF satisfiability and DPLL has been posted here.
  • Compensation class on Wed, Oct 9 6.30-8.00pm 7.00-8.30 pm in CC105.

Course Information

This course has been re-designed (from its earlier avatar) to be a foundational breadth course primarily for students who wish to pursue advanced studies in formal methods and/or pursue research and development projects in this exciting area. The course will also be useful for those desirous of pursuing studies/research in programming languages and program analysis. It will cover a wide breadth of topics in logic, automata, formal proofs, decision procedures and their applications to some formal verification problems. We will review and then build on topics prescribed in the GATE CS syllabus for theory of computation. The course presumes that students have gone/are concurrently going through an undergraduate course on theory of computation, discrete structures and algorithms.
The list of topics to be covered in the course includes:
  • Propositional logic: syntax and semantics, truth table, satisfiability proof systems, equivalences, normal forms, Tseitin encoding
  • FOL (First order logic): syntax and semantics, SAT problem in FOL, proof systems, FOL Theories
  • Simple programming language, small and big step semantics, strongest postcondition, weakest preconditon, Hoare logic, invariants, tools for invariant checking
  • Satisfiability (SAT) solvers for propositional logic, conflict-driven clause learning (CDCL) and optimizations, examples of encoding problems into SAT problems, satisfiability modulo theory (SMT) solvers
  • Linear temporal logic (LTL) and Computation tree logic(CTL): syntax and semantics, normal forms, satisfiability problems
  • (Non)-Deterministic finite-state automata on finite words, subset construction, regular expressions, pumping lemma
  • (Non)-Deterministic finite-state automata on infinite words: omega-regular languages, non-deterministic Buchi automata and LTL, emptiness checking.
  • Basic notions of computability, Turing machines, undecidability

IMPORTANT: Students are required to put in 4 to 6 hours of reading per week beyond the contact hours in class.


What When Where
Lectures Mon 9:30-10:30,
Tue 10:30-11:30
Thu 11:30-12:30
CC 101 (CC-CSE building)
Office hour Wed 16:30-17:30 CC 314 (CC-CSE Building)
(strictly by email appointment)


Midsem 30%
Endterm 50%
Quizes 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 no homeworks but plenty of quizes (including surprise quizes)
  • Each graded homework/quiz will carry equal weightage.
  • 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.
  • If you are unsure about the distinction between copying and discussion, please read this.

Reading Material and References

  • Michael Huth and Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems , Second Edition, Cambridge University Press
  • D. Kroening and O. Strichman, Decision Procedures: An Algorithmic Point of View , 2nd edition, Springer, 2017
  • Javier Esparza, Lecture Notes on Automata Theory: An Algorithmic Approach
  • A. Robinson (Editor), et al 2001. Handbook of Automated reasoning. North Holland, eBook ISBN: 9780080532790
  • Z3 source code

Current Reading List

  • Chapters 1 and 2 of Logic in Computer Science:... by M. Huth and M. Ryan
  • Chapters 1 and 2 of Decision Procedures: ... by D, Kroening and O. Strichman.
  • A set of slides on First Order Logic
  • A note on 2-CNF satisfiability.
  • Slides (Ruben Martins) and slides (Emina Torlak) on CDCL SAT solvers.
  • An excellent chapter on CDCL SAT solving in the Handbook of Satisfiability.
  • Lecture notes of Prof. Krishna S. on NBA and LTL-to-GNBA construction (coming soon ...)
  • Chapter 3 (sections 3.1 and 3.2) of Logic in Computer Science:... by M. Huth and M. Ryan
  • Chapter 11 (sections 11.1, 11.2, 11.3) and Chapter 14 (section 14.3) of Lecture Notes on Automata Theory: An Algorithmic Approach by Javier Esparza
  • Lecture notes of Prof. Akshay on Turing Machines and undecidability (coming soon ...)
  • Chapter 9 (Undecidability) of Introduction ot Automata Theory, Languages and Computation -- the classic text book by J.E. Hopcroft, R. Motwani and J.D. Ullman

Practice Problems ...

Lecture Schedule

Date Topics details
Jul 29 Course overview and prerequisites. The importance of logical reasoning in both theory and practice. Introduction to propositional logic syntax and tree/DAG representations of formulas.
Jul 30 More on syntax and semantics of propositional logic. Evaluating a formula by walking up its DAG representation, and its advantages. Notions of satisfiability, unsatisfiability and validity. Understanding how a decision procedure for satisfiability can be used to check validity and vice versa.
Aug 1 Need for a proof system. Essential components of a proof system: axioms and inference rules. A proof tree as a formal mathematically checkable object. Introduction to natural deduction as a proof system for propositional logic.
Aug 5 More on natural deduction for propositional logic, soundness and completeness of natural deduction, difference between finding a proof and checking a proof. Discussion on how to search for a natural deduction proof and dealing with unboundedness in the search.
Aug 6 Normal forms: CNF and DNF. Resolution as a proof system for CNF formulas: notion of resolvents, iterated generation of resolvents, consequence of empty clause being a resolvent. Example of resolution applied on a satisfiable and an unsatisfiable formula. Maximum number of resolvents derivable from a CNF formula, termination implication for resolution proof system.
Aug 8 More on resolution for propositional logic: proving that a CNF formula is unsatisfiable iff the empty clause can be derived from it by resolution. Resolution as a satisfiability decision procedure.
Aug 12 Institute holiday