Combining model checking and theorem proving to verify parallel processes

Abstract

To overcome the limitations of pure model checking, this verification technique is combined with theorem proving. Large processes are split into components whose correctness w.r.t. local specifications is checked via model checking. The correctness of the composition w.r.t. the global specification is then established by constructing a formal proof in a derivation system with the help of a theorem prover.