| Cumulatives for Safety (2007) | |||||||||||||||
Abstract | |||||||||||||||
| We introduce a proof method for safety properties in the setting of refinement of imperative programs `a la Hoare-He-Sanders and Kinoshita-Power. In order to show that the safety property of the abstract programs implies the corresponding safety property of the concrete program, we introduce a notion of 'semantic cumulative'. This leads to a hybrid method of verification which consists of model checking and theorem proving. To show the safety of the concrete program, our main result says that one has only to show the safety of the abstract program, and that can be done by the model checking technique, thanks to the extraordinary reduction of the number of states. Our main theorem, in turn, can be shown by a theorem prover, if one wants a machine checked verification. As an example, we report our validation of on-the-fly garbage collection using the proposed method. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||