Skip to main content
SpringerLink
Log in

Proof Repositories for Compositional Verification of Evolving Software Systems

Managing Change When Proving Software Correct

  • Chapter
  • First Online:
Transactions on Foundations for Mastering Change I

Part of the book series: Lecture Notes in Computer Science ((TFMC,volume 9960))

Abstract

We propose a new and systematic framework for proof reuse in the context of deductive software verification. The framework generalizes abstract contracts into incremental proof repositories. Abstract contracts enable a separation of concerns between called methods and their implementations, facilitating proof reuse. Proof repositories allow the systematic caching of partial proofs that can be adapted to different method implementations. The framework provides flexible support for compositional verification in the context of, e.g., partly developed programs, evolution of programs and contracts, and product variability.

Partly funded by the EU project H2020-644298 HyVar: Scalable Hybrid Variability for Distributed Evolving Software Systems (http://www.hyvar-project.eu), the EU project FP7-610582 Envisage: Engineering Virtualized Services (http://www.envisage-project.eu), the Ateneo/CSP project RunVar, and the ICT COST Actions IC1402 ARVI (http://www.cost-arvi.eu) and IC1201 BETTY (http://www.behavioural-types.eu), and IoTSec (http://cwi.unik.no/wiki/IoTSec:Home).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We are aware that this basic technique is insufficient to achieve modular verification. Advanced techniques for modular verification, e.g. [1, 22, 34], would obfuscate the fundamental questions considered in this paper and can be superimposed.

  2. 2.

    Not all locations in LS need to appear in the defs. About the ones who do not, nothing is known except what is stated in E.

  3. 3.

    This implies the limitation that no (not even pure) method calls can occur in pre- and postconditions. This could be lifted or worked around in various ways.

  4. 4.

    If i is the label of a method implementation that contains at least one method call, then \(S\Downarrow i,\epsilon \) will always return a non-empty set. More generally, if i is the label of a method implementation and the domain of \(\mathcal {B}\) does not contain all the method calls in i, then \(S\Downarrow i,\mathcal {B}\) will always return a non-empty set.

  5. 5.

    This is not a restriction since, in Java, method overloading is resolved statically.

  6. 6.

    This can be checked straightforwardly by comparing the labels.

References

  1. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27–56 (2004)

    Article  Google Scholar 

  2. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30569-9_3

    Chapter  Google Scholar 

  3. Beckert, B., Hähnle, R.: Reasoning and verification. IEEE Intell. Syst. 29(1), 20–29 (2014)

    Article  Google Scholar 

  4. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  5. Beckert, B., Klebanov, V.: Proof reuse for deductive program verification. In: Third IEEE International Conference on Software Engineering and Formal Methods, pp. 77–86. IEEE Computer Society (2004). http://doi.ieeecomputersociety.org/10.1109/SEFM.2004.10013

  6. Beckert, B., Schmitt, P.H.: Program verification using change information. In: Proceedings, Software Engineering and Formal Methods (SEFM), Brisbane, Australia, pp. 91–99. IEEE Press (2003)

    Google Scholar 

  7. Bettini, L., Damiani, F., Schaefer, I.: Compositional type checking of delta-oriented software product lines. Acta Inform. 50(2), 77–122 (2013). doi:10.1007/s00236-012-0173-z

    Article  MathSciNet  MATH  Google Scholar 

  8. Bruns, D., Klebanov, V., Schaefer, I.: Verification of software product lines with delta-oriented slicing. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 61–75. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18070-5_5

    Chapter  Google Scholar 

  9. Bubel, R., Hähnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 120–134. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45231-8_9

    Google Scholar 

  10. Damiani, F., Dovland, J., Johnsen, E.B., Schaefer, I.: Verifying traits: an incremental proof system for fine-grained reuse. Formal Aspects Comput. 26(4), 761–793 (2014)

    Article  MATH  Google Scholar 

  11. Damiani, F., Owe, O., Dovland, J., Schaefer, I., Johnsen, E.B., Yu, I.C.: A transformational proof system for delta-oriented programming. In: Proceedings of the 16th International Software Product Line Conference (SPLC), vol. 2, pp. 53–60. ACM (2012)

    Google Scholar 

  12. Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. J. Logic Algebraic Program. 79(7), 578–607 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  13. Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Incremental reasoning with lazy behavioral subtyping for multiple inheritance. Sci. Comput. Program. 76(10), 915–941 (2011)

    Article  MATH  Google Scholar 

  14. Dovland, J., Johnsen, E.B., Owe, O., Yu, I.C.: A proof system for adaptable class hierarchies. J. Log. Algebraic Methods Program. 84(1), 37–53 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  15. Dovland, J., Johnsen, E.B., Yu, I.C.: Tracking behavioral constraints during object-oriented software evolution. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 253–268. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34026-0_19

    Chapter  Google Scholar 

  16. Engel, C., Roth, A., Schmitt, P.H., Weiß, B.: Verification of modifies clauses in dynamic logic with non-rigid functions. Technical report 2009–9, Department of Computer Science, University of Karlsruhe (2009)

    Google Scholar 

  17. Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18070-5_2

    Chapter  Google Scholar 

  18. Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_21

    Chapter  Google Scholar 

  19. Hähnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 300–314. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_21

    Chapter  Google Scholar 

  20. Hutter, D., Autexier, S.: Formal software development in MAYA. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 407–432. Springer, Heidelberg (2005). doi:10.1007/978-3-540-32254-2_24

    Chapter  Google Scholar 

  21. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). doi:10.1007/978-3-642-20398-5_4

    Chapter  Google Scholar 

  22. Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006). doi:10.1007/11813040_19

    Chapter  Google Scholar 

  23. Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML reference manual (2009). ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmlrefman.pdf. Draft revision 1.235

  24. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS(LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17511-4_20

    Chapter  Google Scholar 

  25. Leino, K.R.M., Wüstholz, V.: Fine-grained caching of verification results. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 380–397. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_22

    Chapter  Google Scholar 

  26. Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)

    Article  Google Scholar 

  27. Meyer, B.: Applying “design by contract”. IEEE Comput. 25(10), 40–51 (1992)

    Article  Google Scholar 

  28. Müller, P., et al.: The 1st verified software competition: experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154–168. Springer, Heidelberg (2011)

    Google Scholar 

  29. Reif, W., Stenzel, K.: Reuse of proofs in software verification. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 284–293. Springer, Heidelberg (1993). doi:10.1007/3-540-57529-4_61

    Chapter  Google Scholar 

  30. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55–74. IEEE Computer Society (2002)

    Google Scholar 

  31. Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (eds.) SPLC 2010. LNCS, vol. 6287, pp. 77–91. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15579-6_6

    Chapter  Google Scholar 

  32. Schaefer, I., Rabiser, R., Clarke, D., Bettini, L., Benavides, D., Botterweck, G., Pathak, A., Trujillo, S., Villela, K.: Software diversity: state of the art and perspectives. Int. J. Softw. Tools Technol. Transf. 14(5), 477–495 (2012). doi:10.1007/s10009-012-0253-y

    Article  Google Scholar 

  33. Schairer, A., Hutter, D.: Proof transformations for evolutionary formal software development. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 441–456. Springer, Heidelberg (2002). doi:10.1007/3-540-45719-4_30

    Chapter  Google Scholar 

  34. Schmitt, P.H., Ulbrich, M., Weiß, B.: Dynamic frames in java dynamic logic. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 138–152. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18070-5_10

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Technische Universität Darmstadt, Darmstadt, Germany

    Richard Bubel & Reiner Hähnle

  2. Department of Computer Science, University of Torino, Turin, Italy

    Ferruccio Damiani

  3. Department of Informatics, University of Oslo, Oslo, Norway

    Einar Broch Johnsen, Olaf Owe & Ingrid Chieh Yu

  4. Institute for Software Engineering, Technische Universität Braunschweig, Braunschweig, Germany

    Ina Schaefer

Authors
  1. Richard Bubel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ferruccio Damiani
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Reiner Hähnle
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Einar Broch Johnsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Olaf Owe
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Ina Schaefer
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Ingrid Chieh Yu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Reiner Hähnle .

Editor information

Editors and Affiliations

  1. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this chapter

Cite this chapter

Bubel, R. et al. (2016). Proof Repositories for Compositional Verification of Evolving Software Systems. In: Steffen, B. (eds) Transactions on Foundations for Mastering Change I. Lecture Notes in Computer Science(), vol 9960. Springer, Cham. https://doi.org/10.1007/978-3-319-46508-1_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46508-1_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46507-4

  • Online ISBN: 978-3-319-46508-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation