Advertisement

Towards a Notion of Coverage for Incomplete Program-Correctness Proofs

  • Bernhard Beckert
  • Mihai Herda
  • Stefan Kobischke
  • Mattias UlbrichEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)

Abstract

Deductive program verification can give high assurances for program correctness. But incomplete partial proofs do not provide any information as to what degree or with what probability the program is correct.

In this paper, we introduce the concept of state space coverage for partial proofs, which estimates to what degree the proof covers the state space and the possible inputs of the program. Thus, similar to testing, the degree of assurance grows with the effort invested in constructing a correctness proof. The concept brings together deductive verification techniques with runtime techniques used to empirically estimate the coverage. We have implemented a prototypical tool that uses test data to estimate the coverage of partial proofs constructed with the program verification system KeY.

Keywords

Program verification Coverage Sequent proofs 

References

  1. 1.
    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book: From Theory to Practice, LNCS, vol. 10001. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49812-6Google Scholar
  2. 2.
    Ahrendt, W., Chimento, J.M., Pace, G.J., Schneider, G.: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Form. Methods Syst. Des. 51(1), 200–265 (2017)CrossRefGoogle Scholar
  3. 3.
    Ahrendt, W., Gladisch, C., Herda, M.: Proof-based test case generation. In: Ahrendt et al. [1], Chap. 12, pp. 415–451.  https://doi.org/10.1007/978-3-319-49812-6Google Scholar
  4. 4.
    Dwyer, M.B., Filieri, A., Geldenhuys, J., Gerrard, M., Păsăreanu, C.S., Visser, W.: Probabilistic program analysis. In: Cunha, J., Fernandes, J.P., Lämmel, R., Saraiva, J., Zaytsev, V. (eds.) GTTSE 2015. LNCS, vol. 10223, pp. 1–25. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-60074-1_1CrossRefGoogle Scholar
  5. 5.
    Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39 176–210, 405–431 (1935)Google Scholar
  6. 6.
    Grindal, M., Offutt, J., Andler, S.F.: Combination testing strategies: a survey. Softw. Test. Verif. Reliab. 15(3), 167–199 (2005).  https://doi.org/10.1002/stvr.319CrossRefGoogle Scholar
  7. 7.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. SIGACT News 32(1), 66–69 (2001).  https://doi.org/10.1145/568438.568456CrossRefzbMATHGoogle Scholar
  8. 8.
    Kobischke, S.: Sampling-based Execution Coverage Estimation for Partially Proved Java Program Specifications. Master’s thesis, Karlsruhe Institute of Technology (2018)Google Scholar
  9. 9.
    Leavens, G.T., et al.: JML Reference Manual, draft Revision 2344, 31 May 2013Google Scholar
  10. 10.
    ben Nasr Omri, F.: Weighted Statistical Testing based on Active Learning and Formal Verification Techniques for Software Reliability Assessment. Ph.D. thesis, Karlsruhe Institute of Technology (2015). http://digbib.ubka.uni-karlsruhe.de/volltexte/1000050941
  11. 11.
    Wilson, E.B.: Probable inference, the law of succession, and statistical inference. J. Am. Stat. Assoc. 22(158), 209–212 (1927).  https://doi.org/10.1080/01621459.1927.10502953CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Bernhard Beckert
    • 1
  • Mihai Herda
    • 1
  • Stefan Kobischke
    • 1
  • Mattias Ulbrich
    • 1
    Email author
  1. 1.Karlsruhe Institute of TechnologyKarlsruheGermany

Personalised recommendations