Symbolic model checking
Evaluate temporal properties of finite state systems
Extremely successfully for hardware verification
Open question: applicable to large software specifications for reactive systems?
Previous slide
Next slide
Back to first slide
View graphic version