形式化验证方面的研究主题(任意一个均可)

• Overview of Model Checking
• Quick introduction to logic
• Propositional logic, Davis Putnam procedure
• Predicate Calculus
• Natural Deduction proofs
• Property specification using Computation tree logic (CTL)
• Concurrency
• Explicit state model checking
• Fairness
• Binary Decision Diagrams (BDDs)
• Symbolic model checking
• Detailed introduction to model checker SMV
• Linear temporal logic (LTL)
• LTL tableaux construction
• LTL model checking
• Detailed introduction to model checker SPIN

• Program Testing
• SAT based model checking
• Abstraction and compositional reasoning
• Hoare logic and sequential programs
• Automated theorem proving