CSEE E6863
FORMAL VERIF HW SW SYSTEMS
Lect: 2. Introduction to the theory and practice of formal methods for the design and analysis of correct (i.e. bug-free) concurrent and embedded hardware/software systems. Topics include temporal logics; model checking; deadlock and liveness issues; fairness; satisfiability (SAT) checkers; binary decision diagrams (BDDs); abstraction techniques; introduction to commercial formal verification tools. Industrial state-of-art, case studies and experiences: software analysis (C/C /Java), hardware verification (RTL).
Topics
- temporal logics
- model checking
- deadlock and liveness issues
- fairness
- satisfiability (SAT) checkers
- binary decision diagrams (BDDs)
- abstraction techniques
- introduction to commercial formal verification tools
Topics explicitly listed in official catalogue description
Prerequisites & course information
Prerequisites: ( COMS W3261 and COMS W3137 ) or ( COMS W3134 and COMS W3136 )
Sources
- Course catalogue ↗2026-2027