CS719: Topics in Mathematical Foundations of Formal Verification
Autumn 2018


Instructor Supratik Chakraborty email: supratik [AT] cse ...
Teaching Assistant Sparsa Roychowdhury email: sparsa [AT] cse ...

Announcements

  • Please subscribe to moodle for CS 719, and also to piazza for CS 719.

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. This course is also best taken along with CS 433 "Automated Reasoning" offered by Prof. Ashutosh Gupta in the current semester. 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 Tue 15:30-17:00,
Fri 15:30-17:00
SIC 305, KReSIT building
Office hour Thurs 16:30-17:30 CC 314 (New CC-CSE Building)
(strictly by email appointment)

Grading

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 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. If you are unsure about the distinction between copying and discussion, please read this.
  • 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

    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)
    • Slides (parts 1&2) on first-order logic.

    Lecture Schedule

    Date Topics details
    Jul 24 Course overview and prerequisites. The importance of logical reasoning in both theory and practice. Introduction to proofs in propositional logic: what is a proof?
    Jul 27 A proof system for propositional logic, working out a few proofs, soundness of proof rules
    Jul 31 Completeness of propositional proof system for finite sets of formulas
    Aug 1 Compactness theorem for propositional logic and its proof; completeness of propositional logic with infinite sets of formulas as a consequence of compactness
    Aug 3 Application of compactness to show limitations of propositional logic: expressing finiteness, singleton-ness of a set of natural numbers. Introduction to resolution for propositional logic: converting to CNF, Tseitin encoding for equisatisfiable (not equivalent) CNF conversion
    Aug 7 More on resolution in propositional logic: soundness of resolution, example, preliminary discussion on completeness of resolution. Introduction to first order logic (FOL)
    Aug 8 Syntax and semantics of FOL, Notion of structures and bindings/environments, examples
    Aug 10 Graphs as first-order structures, notions of semantic and syntactic entailment, a proof system for FOL, soundness and completeness of proof system, compactness of FOL and some consequences