Comp 681: Formal Methods

Spring 2019

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/15 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/17 Concepts: Propositional logic review
  • Satisfiability and validity
  • Proof methods: truth tables and semantic arguments
  • Normal forms (NNF, CNF, DNF)
 [Reading 1]
Lecture 3 1/22 Concepts: SAT Solvers
  • CDCL Algorithm
  • Highlighting extensions to DPLL
  • Understanding implication graphs
 [Reading 2]
[Reading 3]
Lecture 4 1/24 Concepts: Applications of SAT Solvers
  • How SAT is used today
  • Variants of SAT solvers
 Homework 1 Assigned
[Reading 4]
Lecture 5 1/29 Concepts: Introduction to SMT Solvers
  • Introduction to first-order logic
  • Overview of common theories
 Report project groups
[Reading 5]
Lecture 6 1/31 Concepts: DPLL Framework
  • Offline algorithm
  • Online algorithm
 [Reading 6]
Lecture 7 2/5 Concepts: Finite Model Finding
  • Review first-order logic
  • Kodkod basics
 [Reading 7]
Lecture 8 2/7 Concepts: Alloy Modeling Language
  • Alloy Grammar
  • Signatures and Relations
 [Reading 8]
Lecture 9 2/12 Concepts: Alloy Modeling Language
  • Using Predications, Functions and Assertions
  • Understanding Scope
  • Translation to SAT
 [Reading 8]
- 2/14 Concepts: Work Day
  • TA will run in-class office hours
  • I will be traveling, available by email
 Homework 1 Due: by 11:59pm
Homework 2 Out
Lecture 10 2/19 Concepts: Validating Alloy Models
  • Type of Faults
  • AUnit
 [Reading 9]
Lecture 11 2/21 Concepts: Alloy Case Study
  • Modeling Academia
  • How to generate instances of interest
Lecture 12 2/26 Concepts: Hoare Logic
  • Hoare Triple
  • Inference Rules
 [Reading 10]
Lecture 13 2/28 Concepts: Hoare Logic: Verification Condition Generation
  • Computing Weakest Pre-Condition
  • Computing Verification Conditions
 [Reading 11]
Lecture 14 3/12 Concepts: Verification with Dafny
  • Dafny Grammar
  • Examples in Dafny
 [Reading 12]
Lecture 15 3/14 Concepts: Bounded Verification
  • 4 Basic Steps
  • Using Results for Fault Localization
 [Reading 13]
[Reading 14]
[Reading 15]
Homework 2 Due: by 11:59pm
Lecture 16 3/19 Concepts: Model Checking
  • LTL Grammar
  • CTL Grammar
  • Ex: traffic light in SPIN
 [Reading 16]
[Reading 17]
- 3/21 Honors convocation: No class Homework 3 Out
Lecture 17 3/26 Concept: Model Checking
  • Limitations of traditional model checking
  • Intro to SLAM Model Checker
 [Reading 18]
Lecture 18 3/28 Concepts: Symbolic Execution
  • What is symbolic execution
  • What are the limitations
 [Reading 19]
[Reading 20]
Lecture 19 4/2 Concept: Concolic Execution
  • DART: Directed Automated Random Testing
  • Explicit Path Model Checking
[Reading 21]
[Reading 22]
- 4/4 No Class: Project Work Day
Lecture 20 4/9 Concept: Program Synthesis
  • What is the synthesis problem?
  • Deductive synthesis: a traditional approach
  • Modern synthesis: computer aided development
 [Reading 23]
Lecture 21 4/11 Concepts: Program Synthesis by Enumeration
  • EuSolver
  • ASketch for Alloy
 [Reading 24]
[Reading 25]
[Reading 26]
Homework 3 Due: by 11:59pm
Lecture 22 4/16 Concept: Formal methods in the real world
  • Guest Lecture: VISA
Lecture 23 4/18 Concepts: Angelic Execution
  • Combining imperative and declarative execution
  • Squander: Alloy and Java combined execution
Lecture 24 4/23 Concepts: Program Synthesis for Java
  • JSketch
  • Sketch4J
 [Reading 27]
[Reading 28]
Lecture 25 4/25 Concepts: Solver-Aided Languages
  • Synthesis-aided compilation
  • Rosette case study
 [Reading 29]
[Reading 30]
Lecture 26 4/30 No class: Project work day
  • Prepare for final presentation
  • Prepare demostration
 Presentation Slides Due: by 11:59pm
Lecture 27 5/2 Concepts: Final Project Presentations
5/6 Final Project Turn-In: Project report and source code due by 11:59 pm