Computational Logic, 2018 Fall

Course Information

• Instructor: Hakjoo Oh
• Lecture: 9:00-11:30 on Mondays

Slides

• Course Overview: lec0.pdf
• Propositional Logic: lec1.pdf, lec2.pdf
• First-Order Logic: lec3.pdf, lec4.pdf, lec5.pdf
• Program Verification: lec6.pdf, lec7.pdf, Hoare Logic
• Decision Procedures: lec8.pdf, Equality Theory, Theory of Rationals, Nelson-Oppen

Homework

• Homework 1: hw1.pdf (due 10/01)
• Homework 2 (Reading): SMT: Introduction and Applications (due 10/29, submit 2-pages summary)
• Homework 3: Exercises 1 and 2 in Lecture 7 (due 11/12)

Resources

• SAT/SMT Solvers:
• Tutorial on Z3
• Applications of SAT/SMT Solvers:
  • Symbolic Execution
  • Dynamic Symbolic Execution
  • Bounded Model Checking
  • Smart Contract Verification
  • Automatic Debugging
  • Intelligent Tutoring System
• Related topics:
  • Abstract Interpretation