nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY

verfasst von : Alexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

As formal verification of software systems is a complex task comprising many algorithms and heuristics, modern theorem provers offer numerous parameters that are to be selected by a user to control how a piece of software is verified. Evidently, the number of parameters even increases with each new release. One challenge is that default parameters are often insufficient to close proofs automatically and are not optimal in terms of verification effort. The verification phase becomes hardly accessible for non-experts, who typically must follow a time-consuming trial-and-error strategy to choose the right parameters for even trivial pieces of software. To aid users of deductive verification, we apply machine learning techniques to empirically investigate which parameters and combinations thereof impair or improve provability and verification effort. We exemplify our procedure on the deductive verification system KeY 2.6.1 and specified extracts of OpenJDK, and formulate 53 hypotheses of which only three have been rejected. We identified parameters that represent a trade-off between high provability and low verification effort, enabling the possibility to prioritize the selection of a parameter for either direction. Our insights give tool builders a better understanding of their control parameters and constitute a stepping stone towards automated deductive verification and better applicability of verification tools for non-experts.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math”

Nächstes Kapitel Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB

https://www.key-project.org/applications/program-verification/ and http://i12 www.ira.uka.de/key/download/quicktour/quicktour-2.0.zip.

http://github.com/AlexanderKnueppel/UnderstandingParametersInKeY.

Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification-The KeY Book: From Theory to Practice. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-49812-6CrossRef

Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54, 81–91 (2011)CrossRef

Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification-specification is the new bottleneck. arXiv preprint arXiv:1211.6186 (2012)

Beckert, B., Bormer, T., Grahl, D.: Deductive verification of legacy code. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 749–765. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_53CrossRef

Benavides, D., Trinidad, P., Ruiz-Cortés, A.: Using constraint programming to reason on feature models. In: Proceedings of the International Conference on Software Engineering and Knowledge Engineering (SEKE), pp. 677–682 (2005)

Bowen, J., Stavridou, V.: Safety-critical systems, formal methods and standards. Softw. Eng. J. 8(4), 189–209 (1993)CrossRef

Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. (STTT) 7(3), 212–232 (2005)CrossRef

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. (CSUR) 28(4), 626–643 (1996)CrossRef

10.

Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_2CrossRef

11.

Cohen, M.B., Dwyer, M.B., Shi, J.: Interaction testing of highly-configurable systems in the presence of constraints. In: Proceedings of the 2007 International Symposium on Software Testing and Analysis, pp. 129–139. ACM (2007)

12.

Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_16CrossRef

13.

Darvas, Á., Mehta, F., Rudich, A.: Efficient well-definedness checking. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 100–115. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_8CrossRef

14.

de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273–289. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_16CrossRef

15.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

16.

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). https://doi.org/10.1007/978-3-540-73368-3_21CrossRef

17.

Gladisch, C.D.: Model generation for quantified formulas with application to test data generation. Proc. Int. J. Softw. Tools Technol. Transfer 14(4), 439–459 (2012)CrossRef

18.

Gosling, J.: The Java Language Specification. Addison-Wesley Professional, Boston (2000)MATH

19.

Grebhahn, A., Siegmund, N., Apel, S., Kuckuk, S., Schmitt, C., Köstler, H.: Optimizing performance of stencil code with SPL conqueror. In: Proceedings of the 1st International Workshop on High-Performance Stencil Computations (HiStencils), pp. 7–14 (2014)

20.

Guo, J., Czarnecki, K., Apely, S., Siegmundy, N., Wasowski, A.: Variability-aware performance prediction: a statistical learning approach. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering, pp. 301–311. IEEE Press (2013)

21.

Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1–16:58 (2012)CrossRef

22.

Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. J. Softw. Tools Technol. Transfer 2(4), 366–381 (2000)CrossRef

23.

Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(4), 271–281 (1972)CrossRef

24.

Holthusen, S., Nieke, M., Thüm, T., Schaefer, I.: Proof-carrying apps: contract-based deployment-time verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 839–855. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_58CrossRef

25.

Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. (TSE) 23(5), 279–295 (1997)CrossRef

26.

Hubbers, E., Poll, E.: Reasoning about card tears and transactions in Java Card. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 114–128. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24721-0_8CrossRef

27.

Huisman, M., Mostowski, W.: A symbolic approach to permission accounting for concurrent reasoning. In: 2015 14th International Symposium on Proceedings of the Parallel and Distributed Computing (ISPDC), pp. 165–174. IEEE (2015)

28.

Kienzle, J., Mussbacher, G., Collet, P., Alam, O.: Delaying decisions in variable concern hierarchies. ACM SIGPLAN Not. 52, 93–103 (2016)CrossRef

29.

Knight, J.C., DeJong, C.L., Gibble, M.S., Nakano, L.G.: Why are formal methods not used more widely? In: Proceedings of the Fourth NASA Formal Methods Workshop. Citeseer (1997)

30.

Knüppel, A., Pardylla, C.I., Thüm, T., Schaefer, I.: Experience report on formally verifying parts of openJDK’s API with KeY. In: Proceedings of the Fourth Workshop on Formal Integrated Development Environment. Springer, Heidelberg (2018)

31.

Leavens, G.T., Cheon, Y.: Design by Contract with JML, September 2006

32.

Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML Reference Manual, May 2013

33.

Marché, C., Moy, Y.: The Jessie Plugin for Deductive Verification in Frama-C. INRIA Saclay Île-de-France and LRI, CNRS UMR (2012)

34.

McNemar, Q.: Note on the sampling error of the difference between correlated proportions or percentages. Psychometrika 12(2), 153–157 (1947)CrossRef

35.

Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall Inc., Upper Saddle River (1988)

36.

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

37.

Ochoa, L., González-Rojas, O., Thüm, T.: Using decision rules for solving conflicts in extended feature models. In: Proceedings of the International Conference on Software Language Engineering (SLE), pp. 149–160. ACM, October 2015

38.

Olaechea, R., Stewart, S., Czarnecki, K., Rayside, D.: Modelling and multi-objective optimization of quality attributes in variability-rich software. In: Proceedings of the Fourth International Workshop on Nonfunctional System Properties in Domain Specific Modeling Languages, p. 2. ACM (2012)

39.

Robby, Rodríguez, E., Dwyer, M.B., Hatcliff, J.: Checking JML specifications using an extensible software model checking. Framework 8(3), 280–299 (2006)MATH

40.

Rushby, J.: Formal methods and their role in the certification of critical systems. In: Shaw R. (ed.) Safety and Reliability of Software Based Systems, pp. 1–42. Springer, London (1997). https://doi.org/10.1007/978-1-4471-0921-1_1

41.

Sannella, D.: A survey of formal software development methods. Department of Computer Science, Laboratory for Foundations of Computer Science, University of Edinburgh (1988)

42.

Scheurer, D., Hähnle, R., Bubel, R.: A general lattice model for merging symbolic execution branches. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 57–73. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_5CrossRef

43.

Schumann, J.M.: Automated Theorem Proving in Software Engineering. Springer, Heiedelberg (2001). https://doi.org/10.1007/978-3-662-22646-9CrossRef

44.

Siegmund, N., Grebhahn, A., Apel, S., Kästner, C.: Performance-influence models for highly configurable systems. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 284–294. ACM (2015)

45.

Siegmund, N., Rosenmüller, M., Kuhlemann, M., Kästner, C., Apel, S., Saake, G.: SPL conqueror: toward optimization of non-functional properties in software product lines. Softw. Qual. J. 20(3–4), 487–517 (2012)CrossRef

46.

Thüm, T., Meinicke, J., Benduhn, F., Hentschel, M., von Rhein, A., Saake, G.: Potential synergies of theorem proving and model checking for software product lines. In: Proceedings of the International Software Product Line Conference (SPLC), pp. 177–186. ACM (2014)

47.

Thüm, T., Schaefer, I., Apel, S., Hentschel, M.: Family-based deductive verification of software product lines. In: Proceedings of the International Conference on Generative Programming and Component Engineering (GPCE), pp. 11–20. ACM, September 2012

48.

Thüm, T., Winkelmann, T., Schröter, R., Hentschel, M., Krüger, S.: Variability hiding in contracts for dependent software product lines. In: Proceedings of the Workshop on Variability Modelling of Software-intensive Systems (VaMoS), pp. 97–104. ACM (2016)

49.

Why Development Team: Why: a software verification platform. http://why.lri.fr/. Accessed 16 Dec 2010

50.

Wohlin, C., Runeson, P., Höst, M., Ohlsson, M.C., Regnell, B.: Experimentation in Software Engineering. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29044-2CrossRefMATH

Titel: Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY
verfasst von: Alexander Knüppel
Thomas Thüm
Carsten Immanuel Pardylla
Ina Schaefer
Verlag: Springer International Publishing
Buch: Interactive Theorem Proving
Print ISBN: 978-3-319-94820-1

Electronic ISBN: 978-3-319-94821-8

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94821-8_20

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner