publication . Article . Preprint . 2018

Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)

Lucas C. Cordeiro; Daniel Kroening; Peter Schrammel;
Open Access English
  • Published: 11 Sep 2018
  • Country: New Zealand
Abstract
Empirical evaluation of verification tools by benchmarking is a common method in software verification research. The Competition on Software Verification (SV-COMP) aims at standardization and reproducibility of benchmarking within the software verification community on an annual basis, through comparative evaluation of fully automatic software verifiers for C programs. Building upon this success, here we describe how to re-use the ecosystem developed around SV-COMP for benchmarking Java verification tools. We provide a detailed description of the rules for benchmark verification tasks, the integration of new tools into SV-COMP's benchmarking framework and also g...
Subjects
free text keywords: Computer Science - Logic in Computer Science, Computer Science - Software Engineering, Common method, Java, computer.programming_language, computer, Computer science, Standardization, Software engineering, business.industry, business, Software, Software verification, Systems engineering, Benchmarking
23 references, page 1 of 2

[1] IDC: Smartphone OS Market Share, 2016 Q3. http://www. idc.com/prodserv/smartphone-os-market-share.jsp Accessed 2018-07-29

[2] Bai, G., Ye, Q., Wu, Y., Botha, H., Sun, J., Liu, Y., Dong, J.S., Visser, W.: Towards model checking Android applications. IEEE Trans. Software Eng. 44(6), 595{612 (2018)

[3] Gupta, K.: Why Is Spring More Popular than Other Java Frameworks? https://www.freelancinggig.com/blog/ 2018/04/26/spring-popular-java-frameworks/ Accessed 2018-07-29

[4] O'Hearn, P.W.: Continuous reasoning: Scaling the impact of formal methods. In: LICS, pp. 13{25 (2018)

[5] Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: CAV. LNCS, vol. 10982, pp. 467{486 (2018)

[6] Durumeric, Z., Kasten, J., Adrian, D., Halderman, J.A., Bailey, M., Li, F., Weaver, N., Amann, J., Beekman, J., Payer, M., Paxson, V.: The matter of Heartbleed. In: IMC, pp. 475{488 (2014) [OpenAIRE]

[7] Iosif, R., Dwyer, M.B., Hatcli , J.: Translating java for multiple model checkers: The bandera back-end. Formal Methods in System Design 26(2), 137{180 (2005). doi:10.1007/s10703-005-1491-3 [OpenAIRE]

[8] Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In: ASE, pp. 3{12 (2000)

[9] Kahsai, T., Rummer, P., Sanchez, H., Schaf, M.: JayHorn: A framework for verifying Java programs. In: CAV. LNCS, vol. 9779, pp. 352{358 (2016)

[10] Cordeiro, L.C., Kesseli, P., Kroening, D., Schrammel, P., Trt k, M.: JBMC: A bounded model checking tool for verifying Java bytecode. In: CAV. LNCS, vol. 10981, pp. 183{190 (2018) [OpenAIRE]

[11] Beyer, D.: Software veri cation with validation of results (report on SV-COMP 2017). In: TACAS. LNCS, vol. 10206, pp. 331{349 (2017)

[12] Anand, S., Pasareanu, C.S., Visser, W.: JPF-SE: A symbolic execution extension to Java PathFinder. In: TACAS. LNCS, vol. 4424, pp. 134{138 (2007) [OpenAIRE]

[13] Pasareanu, C.S., Rungta, N.: Symbolic PathFinder: symbolic execution of Java bytecode. In: ASE, pp. 179{180 (2010) [OpenAIRE]

[14] Beyer, D., Lowe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. International Journal on Software Tools for Technology Transfer (to appear) (2017)

[15] Alglave, J., Donaldson, A.F., Kroening, D., Tautschnig, M.: Making software veri cation tools really work. In: ATVA. LNCS, vol. 6996, pp. 28{42 (2011) [OpenAIRE]

23 references, page 1 of 2
Abstract
Empirical evaluation of verification tools by benchmarking is a common method in software verification research. The Competition on Software Verification (SV-COMP) aims at standardization and reproducibility of benchmarking within the software verification community on an annual basis, through comparative evaluation of fully automatic software verifiers for C programs. Building upon this success, here we describe how to re-use the ecosystem developed around SV-COMP for benchmarking Java verification tools. We provide a detailed description of the rules for benchmark verification tasks, the integration of new tools into SV-COMP's benchmarking framework and also g...
Subjects
free text keywords: Computer Science - Logic in Computer Science, Computer Science - Software Engineering, Common method, Java, computer.programming_language, computer, Computer science, Standardization, Software engineering, business.industry, business, Software, Software verification, Systems engineering, Benchmarking
23 references, page 1 of 2

[1] IDC: Smartphone OS Market Share, 2016 Q3. http://www. idc.com/prodserv/smartphone-os-market-share.jsp Accessed 2018-07-29

[2] Bai, G., Ye, Q., Wu, Y., Botha, H., Sun, J., Liu, Y., Dong, J.S., Visser, W.: Towards model checking Android applications. IEEE Trans. Software Eng. 44(6), 595{612 (2018)

[3] Gupta, K.: Why Is Spring More Popular than Other Java Frameworks? https://www.freelancinggig.com/blog/ 2018/04/26/spring-popular-java-frameworks/ Accessed 2018-07-29

[4] O'Hearn, P.W.: Continuous reasoning: Scaling the impact of formal methods. In: LICS, pp. 13{25 (2018)

[5] Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: CAV. LNCS, vol. 10982, pp. 467{486 (2018)

[6] Durumeric, Z., Kasten, J., Adrian, D., Halderman, J.A., Bailey, M., Li, F., Weaver, N., Amann, J., Beekman, J., Payer, M., Paxson, V.: The matter of Heartbleed. In: IMC, pp. 475{488 (2014) [OpenAIRE]

[7] Iosif, R., Dwyer, M.B., Hatcli , J.: Translating java for multiple model checkers: The bandera back-end. Formal Methods in System Design 26(2), 137{180 (2005). doi:10.1007/s10703-005-1491-3 [OpenAIRE]

[8] Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In: ASE, pp. 3{12 (2000)

[9] Kahsai, T., Rummer, P., Sanchez, H., Schaf, M.: JayHorn: A framework for verifying Java programs. In: CAV. LNCS, vol. 9779, pp. 352{358 (2016)

[10] Cordeiro, L.C., Kesseli, P., Kroening, D., Schrammel, P., Trt k, M.: JBMC: A bounded model checking tool for verifying Java bytecode. In: CAV. LNCS, vol. 10981, pp. 183{190 (2018) [OpenAIRE]

[11] Beyer, D.: Software veri cation with validation of results (report on SV-COMP 2017). In: TACAS. LNCS, vol. 10206, pp. 331{349 (2017)

[12] Anand, S., Pasareanu, C.S., Visser, W.: JPF-SE: A symbolic execution extension to Java PathFinder. In: TACAS. LNCS, vol. 4424, pp. 134{138 (2007) [OpenAIRE]

[13] Pasareanu, C.S., Rungta, N.: Symbolic PathFinder: symbolic execution of Java bytecode. In: ASE, pp. 179{180 (2010) [OpenAIRE]

[14] Beyer, D., Lowe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. International Journal on Software Tools for Technology Transfer (to appear) (2017)

[15] Alglave, J., Donaldson, A.F., Kroening, D., Tautschnig, M.: Making software veri cation tools really work. In: ATVA. LNCS, vol. 6996, pp. 28{42 (2011) [OpenAIRE]

23 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Article . Preprint . 2018

Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)

Lucas C. Cordeiro; Daniel Kroening; Peter Schrammel;