This course is about logic and its application to software engineering. Briefly, the course will cover the following topics:

For more detailed course description and philosophy, please click here.

Date/Time/Place:  Fridays/11:30 AM-2:20 PM/EIT-3141

Project Demo: December 2nd, 2013. 15:00 - 18:00 Hours, Room EIT 3141

Final Exam: December 5th, 2013, 12:30 - 15:00 Hours, Room EIT 3151

Acknowledgements: Some of the course material has been prepared based on lectures created by Professor Isil Dillig, and appropriate papers/books (see below).

Date
Lectures
Notes, Links, Papers, Books
Fri Sep 13, 2013

Lecture 1
  • What is logic? Foundational concepts
  • Motivation for logic in software engg.
  • Propositional logic basics
Lecture 2
  • Propositional logic continued
  • Normal forms (CNF, NNF,..)

  1. An Introduction to Mathematical Logic by Herbert Enderton

  2. Model Theory by Wilfrid Hodges

  3. Calculus of Computation by Bradley and Manna

  4. Decision Procedures: An Algorithmic Point of View by Kroening and Strichman
Fri Sep 20, 2013

Brief review of Lecture 1 and 2

Lecture 2 continued
  • Tseitin translation (CNF conversion)
  • DPLL SAT Solver
Lecture 3
  • Concolic testing: an application

  1. References to the DPLL algorithm and related work

  2. References to concolic testing

  3. Symbolic Execution for Software Testing: Three Decades Later by Sen and Cadar

  4. Tools: KLEE (symbolic-execution tester), LLVM (program analysis platform)

  5. Papers on automatic exploit construction using SAT/SMT solvers: Sean Heelan and David Brumley (specifically focus on the BAP paper, Automatic Exploit Generation (AEG) paper, and the Q paper.)
Sat Sep 21, 2013
(Start date for assignment #1)
Assignment #1
 Due Fri Oct 4th, 2013 at midnight. Submit PDFs only. Submit directly to the Learn system.
Fri Sep 28, 2013
NO CLASS

Fri Oct 4, 2013
Lecture 4
  • Modern conflict-driven clause-learning (CDCL) SAT solvers
  1. Grasp paper

  2. ZChaff paper (ICCAD 2001)

  3. ZChaff Longer Paper (CAV 2002)

  4. MiniSAT Webpage
Fri Oct 11, 2013
  • Introduction to complexity theory, reductions, complexity classes

Lecture 5
  • CDCL SAT solvers continued
  1. Introduction to Theory of Computation book by Michael Sipser
Fri Oct 18, 2013
Lecture 6
  • First-order logic (FOL) and theories
Lecture 7
  • FOL continued (Decidability, compactness,...)
  1. Enderton book on logic for an introduction to first-order logic, theories,...
Fri Oct 25, 2013
Lecture 7 (continued)

Lecture 8
  • Intro to SMT solvers
  1. Enderton book on logic for an introduction to first-order logic, theories,...

  2. Terry Tao's lucid exposition of the completeness and compactness theorems
Fri Nov 1, 2013
Lecture 9
  • Detailed definition of theories (signature, axioms,...) of interest. Definition of meta properties, e.g., completeness of theories
Lecture 10
  • Theory of uninterpreted functions (Core solver)

Sun Nov 3, 2013 (assignment start date)
Assignment #2
This assignment is due on Nov. 24, 2013. Submit PDFs only. Submit directly to the Learn system.
Fri Nov 8, 2013
Lecture 11
  • Combination of decision procedures (a la Nelson-Oppen,...)
Lecture 12
  • Theory of bit-vectors and arrays


Mon Nov 11, 2013
Lecture 13
  • Decision Procedure for the Rationals (Decision version of Simplex)

Fri Nov 15, 2013
Lecture 14
  • IC3 Model Checking Algorithm (Guest lecture by Dr. Shoham Ben-David)

Fri Nov 22, 2013
Lecture 15
  • Theories of Strings, and String Solvers

Fri Nov 29, 2013
Lecture 16
  • DPLL(T) and Programmatic SAT Solver