Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Weyuker, E.J., Ostrand, T.J.: Theories of Program Testing and the Application of Revealing Subdomains. IEEE Transactions on Software Engineering 6, 236–246 (1980)
Hamlet, D., Taylor, R.: Partition Testing Does Not Inspire Confidence. IEEE Transactions on Software Engineering 16, 1402–1411 (1990)
Goodenough, J.B., Gerhart, S.L.: Toward a Theory of Test Data Selection. IEEE Transactions on Software Engineering 1, 156–173 (1975)
Howden, W.E.: Reliability of the Path Analysis Testing Strategy. IEEE Transactions on Software Engineering 2, 208–215 (1976)
Richardson, D., Clarke, L.: Partition Analysis: A Method Combining Testing andVerification. IEEE Transactions on Software Engineering 11, 1477–1490 (1985)
Ahrendt, W., Baar, T., Beckert, B., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Schmitt, P.H.: The KeY system: Integrating object-oriented design and formal methods. In: Kutsche, R.D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 327–330. Springer, Heidelberg (2002)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Beckert, B.: A dynamic logic for the formal verification of Java Card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6–24. Springer, Heidelberg (2001)
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)
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)
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)
Geller, M.M.: Test data as an aid in proving program correctness. Communications of the ACM 21, 368–375 (1978)
Nimmer, J.W., Ernst, M.D.: Automatic generation of program specifications. In: Proceedings of the international symposium on Software testing and analysis, pp. 229–239. ACM Press, New York (2002)
Slind, K.: Derivation and use of induction schemes in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 275–290. Springer, Heidelberg (1997)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hähnle, R., Wallenburg, A. (2004). Using a Software Testing Technique to Improve Theorem Proving. In: Petrenko, A., Ulrich, A. (eds) Formal Approaches to Software Testing. FATES 2003. Lecture Notes in Computer Science, vol 2931. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24617-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-24617-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20894-5
Online ISBN: 978-3-540-24617-6
eBook Packages: Springer Book Archive