CS474: Logic in Computer Science Spring 2023
Madhusudan Parthasarathy
Resources

  • Notes on Program Verification by Madhusudan: Semantics, Symbolic Evaluation, Bounded Model-checking, VC-generation based Verification, and Hoare Logic -- September 29, 2026; this is a ``living'' changing document; always download latest version as the course proceeds.

  • Logic in CS - Course Notes, by P. Madhusudan and Mahesh Viswanathan (ensure current version and 2026); this is a ``living'' changing document; always download latest version as the course proceeds.

  • Satisfiability Modulo Theories, Clarke Barrett and Cesare Tinelli

  • Z3 Tutorial Online

  • A Mathematical Introduction to Logic, by H. B. Enderton; the link gives an online copy of the book using your netid/password.

  • Calculus of Computation, by Bradley and Manna
    Available from Springer's website from university domain.

  • On the unusual effectiveness of logic in computer science, by Harper, Halpern, Immerman, Kolaitis, Vardi, and Vianu.

  • An Introduction to Logic, by Madhavan Mukund and S. P. Suresh

  • Moshe Vardi's course on logic in computer science; see Lecture Notes

  • The Quest for Efficient Boolean Satisfiability Solvers by Sharad Malik (slides) . See also related paper.

  • Kumar's lecture notes, Lecture 2 and Lecture 3 on MSO on finite words and its equivalence with regular languages (In Chapter 3, omit Section 1 on Stratification of FO formulas).

  • Languages, Automata, and Logic by Wolfgang Thomas.

  • Elements of Finite Model Theory by Leonid Libkin.

  • Notes on Resolution by Toniann Pitassi. Presents completeness of resolution using a decision tree view.

  • An algorithm for reasoning about equality by Shostak.

  • Fast decision procedures based on congruence closure by Nelson and Oppen.

  • Work on decidable synthesis for separation of finite models using FOL formulas (as well as many other logics) and a meta-theorem about a class of such decidability results by Paul Krogmeier and Madhusudan Parthasarathy

    •