An analytical survey of modern verification methods for sequential functional, reactive, and distributed systems is presented. The emphasis is on methods based on properties of abstract interpretation, transition systems, and Petri nets.