We present a modular technique to prove invariants of state-transition systems in a deductive framework. We show how the semantic knowledge fo the given problem can be generically used to decompose the problem into modular tasks which can be successfully tackled with the help of techniques developed in the field of inductive theorem proving. As an example we present the mechanical verification of the invariant of a case study specifying a generic elevator.
展开▼
