Comp 681: Formal Methods

Spring 2020

TR 11:00 to 12:15 in McNair 129

Home Course Info Course Project Readings Tools

Instructor

Schedule

Lecture Date Description Course Materials
Lecture 1 1/14 Concepts: What is formal methods?
  • Definition and applications of specifications
  • Definition and applications of verification
  • Definition and applications of synthesis
 [Reading 0]
Lecture 2 1/16 Concepts: Propositional logic review
  • Satisfiability and validity
  • Proof methods: truth tables and semantic arguments
  • Normal forms (NNF, CNF, DNF)
 [Reading 1]
Lecture 3 1/21 Lab: Satisfiable, Valid and Encodings
  • Propositional Logic Arguments
  • Encoding a Logic Problem Into Propositional Logic
Lecture 4 1/23 Concepts: How SAT solvers work
  • CDCL Algorithm
  • Example: Houses Logic Problem
  • Example: Installing Dependencies
 [Reading 2]
[Reading 3]
Lecture 5 1/28 Concepts: SMT Solvers - Basics
  • Limitations of SAT Solvers
  • Exploration of Theories
  • Example: System of Equations
  • Example: Word Problems
 [Reading 4]
Lecture 6 1/30 Lab: SMT Solvers - Basics
  • Warm Up: A SAT Problem with the Power of a SMT Solver
  • A Geometric System of Equations
  • Alphanumeric Puzzles
 Project Proposal: Due 11:59 pm
Lecture 7 2/4 Concepts: Solving CS Algorithms with SMT
  • Job Scheduling
  • NP Complete Aglorithms
  • Generating SMT models from the problem's patterns: Addressing the concrete nature of SMT Solvers
 [Reading 5]
Lecture 8 2/6 Lab: Solving CS Algorithms with SMT
  • Tiling Problem
  • Topological Sort
Lecture 9 2/11 Concepts: Program Verification with SMT
  • Contract-Based Verification
  • Equivalence-Based Verification
 [Reading 6]
[Reading 7]
Lecture 10 2/13 Lab: Program Verification with SMT
  • Developing Pre-/Post-Conditions
  • Verifying BankAccount Functionality
  • Equivalence: Different Implemtnations to Return Largest Value
Lecture 11 2/18 Lab: N-Queens
  • Solve the 4-Queens program in Z3
 [Reading 6]
[Reading 7]
Lecture 12 2/20 Lab: N-Queens
  • Develop a program to generate the X-Queens encoding in Z3 for any "X"
 Status Report 1: Due 11:59 pm
Lecture 13 2/25 Concepts: Introduction to First-Order Logic
  • Limitations of Propositional Logic
  • Quantified Formulas
  • Formulas Utiliziing Predicates and Sets
 [Reading 8]
Lecture 14 2/27 Lab: Introduction to First-Order Logic
  • Encoding English into FOL
  • Encoding Requirements into FOL
  • Encoding Expressions Using Set Operators
Lecture 15 3/10 Concepts: Introduction to Alloy
  • Signatures
  • Relations
  • Scope-bounded Analysis
 [Reading 9]
Lecture 16 3/12 Lab: Introduction to Alloy
  • Building signatures for different problem scopes
  • Building relations for different problem scopes
Lecture 17 3/17 Concepts: Alloy Predicates
  • Review: Relational Algebra
  • Building FOL formulas in Alloy
 [Reading 10]
Lecture 18 3/19 Lab: Alloy Predicates
  • Extending a singly-linked list model
Lecture 19 3/24 Concepts: Alloy Predicates
  • Depth: Binary Search Tree
  • Incremental model development
 [Reading 11]
Lecture 20 3/26 Lab: Alloy Predicates
  • Model a red-black tree