how would model checking differ for software?

sequential

focus not on concurrency

relational

state itself is relational

essence of Z, RDB, OO

incremental & modular

global operations

declarative style

abstract

all software is infinite state

Previous slide

Next slide

Back to first slide

View graphic version