University of Cincinnati Logo
 

20-CS-626 - Formal Methods
School of Computing Sciences and Informatics

Probable Schedule
   
  Week   Topics Reading
3/28
  Introduction: What can FV accomplish? Examples. Low-level tools (Satisfiability and BDDs). Model checking, Theorem proving.  
 Franco-Weaver-Schlipf 
 SBSAT manual
 SBSAT description
4/4
  Bounded model checking using SBSAT  
 SAT/BDDs
 Traversals
 BMC-SBSAT
 Clarke, Biere, ...
4/11
  Model Checking  
 Symbolic Model Checking
 Kripke
 Model Checking
4/18
  SAT, BDDs, AIGs, SBSAT, minisat  
 BDD
 SAT
 AIG
 SBSAT
minisat
4/25
  Review, Exam  
- - -
5/2
  ACL2 - a modern theorem prover  
 The prover
 Manual
5/9
  ACL2 used in formal verification  
 Examples
5/16
  Correct by construction, Cryptol  
 Cheaper_Better
 Secure System
5/23
  Cryptol  
 Prog. Guide
 Tools Guide
 Tutorial
5/30
  Cryptol, Equivalence checking  
Equivalence Checking
ERC
MainStreet
Paul Erdos
NIT
Ladies on Campus
Oscar Robinson