Formal Methods, 2017 Fall

Course Information

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

Slides

• Overview: lec0.pdf
• Propositional Logic: lec1.pdf
• First-Order Logic: lec2.pdf
• First-Order Theories: lec3.pdf, lec4.pdf
• Program Verification: lec5.pdf
• Program Analysis: lec6.pdf, lec7.pdf, lec8.pdf
• Symbolic Execution: lec9.pdf

Homework

• HW1 (due 10/30, in class): hw1.pdf

Reading

• Z3 SMT Solver
• Introductory Articles
• Satisfiability modulo theories: introduction and applications
• Boolean Satisfiability: From Theoretical Hardness to Practical Success
• The Science of Brute Force
• Research Papers
• A static analyzer for large safety-critical software
• The Octagon Abstract Domain
• Scalable error detection using boolean satisfiability
• Combinatorial sketching for finite programs
• Synthesis of loop-free programs
• Oracle-guided component-based program synthesis
• Cause clue clauses: error localization using maximum satisfiability
• Automated Whitebox Fuzz Testing