Using a Software Testing Technique to Improve Theorem Proving
Most efforts to combine formal methods and software testing go in the direction of exploiting formal methods to solve testing problems, most commonly test case generation. Here we take the reverse viewpoint and show how the technique of partition testing can be used to improve a formal proof technique (induction for correctness of loops). We first compute a partition of the domain of the induction variable, based on the branch predicates in the program code of the loop we wish to prove. Based on this partition we derive a partitioned induction rule, which is (hopefully) easier to use than the standard induction rule. In particular, with an induction rule that is tailored to the program to be verified, less user interaction can be expected to be required in the proof. We demonstrate with a number of examples the practical efficiency of our method.
KeywordsInduction Hypothesis User Interaction Software Test Dynamic Logic Induction Rule
Unable to display preview. Download preview PDF.
- 9.Burstall, R.M.: Program proving as hand simulation with a little induction. In: Rosenfeld, J.L. (ed.) Proceedings of IFIP Congress 1974, Information Processing 1974, pp. 201–210 (1974)Google Scholar
- 10.Hähnle, R., Heisel, M., Reif, W., Stephan, W.: An interactive verification system based on dynamic logic. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 306–315. Springer, Heidelberg (1986)Google Scholar
- 11.Heisel, M., Reif, W., Stephan, W.: Program verification by symbolic execution and induction. In: Proc. 11th German Workshop on Artifical Intelligence. Informatik Fachberichte, vol. 152, pp. 201–210. Springer, Heidelberg (1987)Google Scholar
- 15.Claessen, K., Hähnle, R., Mårtensson, J.: Verification of hardware systems with first-order logic. In: Sutcliffe, G., Pelletier, J., Suttner, C., eds.: Proc. Problems and Problem Sets Workshop, affiliated to CADE-18, Copenhagen, DIKU, University of Copenhagen, Denmark, Technical Report (2002)Google Scholar