Using a Software Testing Technique to Improve Theorem Proving

  • Reiner Hähnle
  • Angela Wallenburg
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2931)


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.


Induction Hypothesis User Interaction Software Test Dynamic Logic Induction Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Hamlet, D., Taylor, R.: Partition Testing Does Not Inspire Confidence. IEEE Transactions on Software Engineering 16, 1402–1411 (1990)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Goodenough, J.B., Gerhart, S.L.: Toward a Theory of Test Data Selection. IEEE Transactions on Software Engineering 1, 156–173 (1975)MathSciNetGoogle Scholar
  4. 4.
    Howden, W.E.: Reliability of the Path Analysis Testing Strategy. IEEE Transactions on Software Engineering 2, 208–215 (1976)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Richardson, D., Clarke, L.: Partition Analysis: A Method Combining Testing andVerification. IEEE Transactions on Software Engineering 11, 1477–1490 (1985)CrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 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. 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. 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
  12. 12.
    Geller, M.M.: Test data as an aid in proving program correctness. Communications of the ACM 21, 368–375 (1978)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Reiner Hähnle
    • 1
  • Angela Wallenburg
    • 1
  1. 1.Department of Computing ScienceChalmers University of Technology and Göteborg UniversityGöteborgSweden

Personalised recommendations