[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

KIV: overview and VerifyThis competition

  • VerifyThis 2012
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Members of our research group participated in the VerifyThis competition at FM 2012 in Paris using the interactive specification and verification system KIV. In this article we describe the KIV verification system and its latest additions. We discuss our solutions to the three VerifyThis problems and which features of KIV were used in solving them. We also report on our findings from performing the proofs.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16

Similar content being viewed by others

Notes

  1. http://fm2012.verifythis.org/

  2. The semicolon in the parameter list separates input and reference parameters, so that assignments to the result in the body of the procedure are visible to the caller.

  3. Note that one needs to carefully track polarities of formulas here, as for example skolemization of \(\exists \) is only possible for positive polarity.

  4. This takes up a proposal of a reviewer.

  5. Note that the \(k\) used in the formula is one higher than the number used in Fig. 14. This means that \(k\) is \(0\) instead of \(-1\) at the end of the loop. Thus, we can stay within natural numbers.

  6. Since these proofs were done last, they were not done as separate lemmas, but as part of the proof of (5) and (6).

  7. http://verifythis2012.cost-ic0701.org/solutions.

References

  1. Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalization by evaluation. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (THOL 08), vol. 5170, pp. 39–54. Springer LNCS, Berlin (2008)

  2. Bäumler, S., Schellhorn, G., Tofan, B., Reif, W.: Proving linearizability with temporal logic. FAC J 23(1), 91–112 (2011)

    MATH  Google Scholar 

  3. Börger, E., Stärk, R.F.: Abstract state machines—a method for high-level system design and analysis. Springer, Berlin (2003)

  4. Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filliatre, J. C., Grigore, R., Huisman, M., Klebanov, V., Marche, C., Monahan, R., Mostowski, W.I., Poiikarpova, N., Scheben, C., Schellhorn, G., Tofan, B., Tschannen, J., Ulbrich, M.: The cost ic0701 verification competition 2011. In: International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2011, vol. 7421, pp. 3–21. Springer, Berlin (2012)

  5. Burstall, R.M.: Program proving as hand simulation with a little induction. Inf. Process. 74, 309–312 (1974)

    Google Scholar 

  6. Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanising a correctness proof for a lock-free concurrent stack. In: Proceedings of FMOODS 2008, Oslo, vol. 5051, pp. 78–95. Springer LNCS, Berlin (2008)

  7. Ernst, G., Schellhorn, G., Haneberg, D., Pfähler, J., Reif, W.: Verification of a virtual filesystem switch. In: Proceedings of Verified Software: Theories, Tools, Experiments, vol. 8164, pp. 242–261. Springer, Berlin (2014)

  8. Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Proceedings of the Symposium on Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society, New York (1967)

  9. Fuchß, T., Reif, W., Schellhorn, G., Stenzel, K.: Three Selected Case Studies in Verification. In: Broy, M., Jähnichen, S.: (eds.) KORSO: Methods, Languages, and Tools for the Construction of Correct Software—Final Report, vol. 1009. Springer LNCS, Berlin (1995)

  10. Grandy, H., Bischof, M., Schellhorn, G., Reif, W., Stenzel, K.: Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code. In: FM 2008: 15th International Symposium on Formal Methods, vol. 5014. Springer LNCS, Berlin (2008)

  11. Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Börger, E. (ed.) Specification and validation methods, pp. 9–36. Oxford Univ. Press, Oxford (1995)

  12. Haneberg, D., Bäumler, S., Balser, M., Grandy, H., Ortmeier, F., Reif, W., Schellhorn, G., Schmitt, J., Stenzel, K.: The user interface of the KIV verification system—as system description. Electronic Notes in Theoretical Computer Science UITP special issue (2006)

  13. Haneberg, D., Moebius, N., Reif, W., Schellhorn, G., Stenzel, K.: Mondex: engineering a provable secure electronic purse. Int. J. Softw. Inf. 5(1):159–184 (2011). http://www.ijsi.org

  14. Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In: Gabbay, D., Guenther, F., (eds.) Handbook of philosophical logic, vol. 4, , 2nd edn, pp. 99–217. Kluwer Academic Publishers, Dordecht (2002)

  15. Huisman, M., Klebanov, V., Monahan, R.: On the organisation of program verification competitions. In: Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE), CEUR Workshop Proceedings, vol. 873 CEUR-WS.org (2012)

  16. Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP’83, pp. 321–332. North-Holland, Amsterdam (1983)

  17. Web presentation of the KIV solutions for the VerifyThis Competition, 2012. http://www.informatik.uni-augsburg.de/swt/projects/verifythis-competition-2012

  18. Manber, U., Myers, G.: Suffix Arrays: a new method for on-Line string searches. In Proceedings of the first annual ACM-SIAM symposium on Discrete algorithms, SODA ’90, pp. 319–327. Society for Industrial and Applied Mathematics (1990)

  19. Manna, Z., Waldinger, R.: Is “sometime” sometimes better than “always”?: intermittent assertions in proving program correctness. Commun. ACM 21(2), 159–172 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  20. Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. IEEE Comput. 18(2), 10–19 (1985)

    Article  Google Scholar 

  21. Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification (CAV), vol. 1102. Springer LNCS, Berlin (1996)

  22. Pfähler, J., Ernst, G., Schellhorn, G., Haneberg, D., Reif, W.: Formal specification of an erase block management layer for flash memory. In: Bertacco, V., Legay, A. (eds.) Hardware and software: verification and testing, vol. 8244, pp. 214–229. Springer International Publishing LNCS, Berlin (2013)

  23. Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, vol. II, pp. 13–39. Kluwer, Dordrecht (1998)

  24. Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, vol. II Systems and Implementation Techniques. Interactive Theorem Proving, Chap. 1, pp. 13–39. Kluwer Academic Publishers, Dordrecht (1998)

  25. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS, pp. 55–74. IEEE Computer Society, New York (2002)

  26. Robinson, P., Staples, J.: Formalizing a hierarchical structure of practical mathematical reasoning. J. Logic Comput. 3(1), 47–61 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  27. Schellhorn, G., Ahrendt, W.: The WAM case study: verifying compiler correctness for prolog with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, vol. III. Applications, Automated Theorem Proving in Software Engineering, Chap. 3, pp. 165–194. Kluwer Academic Publishers, Dordecht (1998)

  28. Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A systematic verification approach for Mondex electronic purses using ASMs. In: Glässer, U., Abrial, J.-R. (eds.) Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, vol. 5115, pp. 93–110. Springer LNCS, Berlin (2009)

  29. Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME), pp. 99–106. IEEE Computer Society Press, New York (2011)

  30. Schierl, A., Schellhorn, G., Haneberg, D., Reif, W.: Abstract specification of the UBIFS file system for flash memory. In: Proceedings of FM 2009: Formal Methods, vol. 5850, pp. 190–206. Springer LNCS, Berlin (2009)

  31. Stenzel, K.: Verification of Java Card Programs. PhD thesis, Universität Augsburg, Fakultät für Angewandte Informatik, http://www.opus-bayern.de/uni-augsburg/volltexte/2005/122/ (2005)

  32. Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam (1969)

  33. Tofan, B., Schellhorn, G., Reif, W.: Formal verification of a lock-free stack with hazard pointers. In Proc. ICTAC, vol. 6916, pp. 239–255. Springer LNCS, Berlin (2011)

  34. Tofan, B., Schellhorn, G., Reif, W.: Local rely-guarantee conditions for linearizability and lock-freedom. Karlsruhe Reports in Informatics 2011–26, Karlsruhe Institute of Technology (2011)

  35. Tuerk, T.: Local reasoning about while-loops. In: Müller, P., Naumann, D., Yang, H. (eds.) Proceedings, VS-Theory Workshop of VSTTE 2010, pp. 29–39 (2010)

  36. The Alloy Project. http://alloy.mit.edu

  37. Xu, Q., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. FAC J 9(2), 149–174 (1997)

    MATH  Google Scholar 

Download references

Acknowledgments

We thank the organizers for providing interesting problems and for the opportunity to discuss the solutions with the other participants after the competition. For us, this led to a better understanding of the difficulties involved and how they were tackled by individual teams and their tools. We also thank the reviewers for their constructive reviews. They have led to small improvements and extensions for two of the case studies.

Author information

Authors and Affiliations

  1. Institute for Software and Systems Engineering, Augsburg University, Augsburg, Germany

    Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg & Wolfgang Reif

Authors
  1. Gidon Ernst
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jörg Pfähler
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gerhard Schellhorn
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Dominik Haneberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Wolfgang Reif
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jörg Pfähler.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Ernst, G., Pfähler, J., Schellhorn, G. et al. KIV: overview and VerifyThis competition. Int J Softw Tools Technol Transfer 17, 677–694 (2015). https://doi.org/10.1007/s10009-014-0308-3

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-014-0308-3

Keywords

Search

Navigation