Advertisement

Abstract

SV-COMP 2015 marks the start of a new epoch of software verification: In the 4th Competition on Software Verification, software verifiers produced for each reported property violation a machine-readable error witness in a common exchange format (so far restricted to reachability properties of sequential programs without recursion). Error paths were reported previously, but always in different, incompatible formats, often insufficient to reproduce the identified bug, and thus, useless to the user. The common exchange format and the support by a large set of verification tools that use the format will make a big difference: One verifier can re-verify the witnesses produced by another verifier, visual error-path navigation tools can be developed, and here in the competition, we use witness checking to make sure that a verifier that claimed a found bug, had really found a valid error path. The other two changes to SV-COMP that we made this time were (a) the addition of the new property, a set of verification tasks, and ranking category for termination verification, and (b) the addition of two new categories for reachability analysis: Arrays and Floats. SV-COMP 2015, the fourth edition of the thorough comparative evaluation of fully-automatic software verifiers, reports effectiveness and efficiency results of the state of the art in software verification. The competition used 5803 verification tasks, more than double the number of SV-COMP’14. Most impressively, the number of participating verifiers increased from 15 to 22 verification systems, including 13 new entries.

Keywords

Software Verification Bound Model Check Error Path Reachability Property Jury Member 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Beyer, D.: Competition on software verification (SV-COMP). In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012)Google Scholar
  2. 2.
    Beyer, D.: Second competition on software verification. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 594–609. Springer, Heidelberg (2013)Google Scholar
  3. 3.
    Beyer, D.: Status report on software verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 373–388. Springer, Heidelberg (2014)Google Scholar
  4. 4.
    Beyer, D., Löwe, S., Wendler, P.: Benchmarking and resource measurement (2015) (unpublished manuscript)Google Scholar
  5. 5.
    Beyer, D., Wendler, P.: Reuse of verification results: Conditional model checking, precision reuse, and verification witnesses. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 1–17. Springer, Heidelberg (2013)Google Scholar
  6. 6.
    Cassez, F., Matsuoka, T., Pierzchalski, E., Smyth, N.: Perentie: Modular trace refinement and selective value tracking (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 438–441. Springer, Heidelberg (2015)Google Scholar
  7. 7.
    Chen, Y.-F., Hsieh, C., Tsai, M.-H., Wang, B.-Y., Wang, F.: CPArec: Verifying recursive programs via source-to-source program transformation (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 425–427. Springer, Heidelberg (2015)Google Scholar
  8. 8.
    Dangl, M., Löwe, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 422–424. Springer, Heidelberg (2015)Google Scholar
  9. 9.
    Gonzalez-de-Aledo, P., Sanchez, P.: FramewORk for embedded system verificaTion (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 428–430. Springer, Heidelberg (2015)Google Scholar
  10. 10.
    Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: A framework for verifying C programs (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 446–449. Springer, Heidelberg (2015)Google Scholar
  11. 11.
    Haran, A., Carter, M., Emmi, M., Lal, A., Qadeer, S., Rakamarić, Z.: SMACK+Corral: A modular verifier (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 450–453. Springer, Heidelberg (2015)Google Scholar
  12. 12.
    Heizmann, M., Dietsch, D., Leike, J., Musa, B., Podelski, A.: Ultimate Automizer with Array Interpolation (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 454–456. Springer, Heidelberg (2015)Google Scholar
  13. 13.
    Holík, L., Hruška, M., Lengál, O., Rogalewicz, A., Šimáček, J., Vojnar, T.: Forester: Shape analysis using tree automata large (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 431–434. Springer, Heidelberg (2015)Google Scholar
  14. 14.
    Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: A lazy sequentialization tool for C (Competition contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 398–401. Springer, Heidelberg (2014)Google Scholar
  15. 15.
    Kroening, D., Tautschnig, M.: CBMC: C bounded model checker (Competition contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014)Google Scholar
  16. 16.
    Le, T.C., Qin, S., Chin, W.-N.: Termination and non-termination specification inference In: PLDI 2015. ACM (2015) (unpublished manuscript)Google Scholar
  17. 17.
    Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22 (Competition contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 405–407. Springer, Heidelberg (2014)Google Scholar
  18. 18.
    Muller, P., Peringer, P., Vojnar, T.: Predator hunting party (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 442–445. Springer, Heidelberg (2015)Google Scholar
  19. 19.
    Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Unbounded Lazy-CSeq: A lazy sequentialization tool for C programs with unbounded context switches (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 460–462. Springer, Heidelberg (2015)Google Scholar
  20. 20.
    Nutz, A., Dietsch, D., Mohamed, M.M., Podelski, A.: Ultimate Kojak (Competition Contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 457–459. Springer, Heidelberg (2015)Google Scholar
  21. 21.
    Rocha, H., Barreto, R., Cordeiro, L., Neto, A.D.: Understanding programming bugs in ANSI-C software using bounded model checking counter-examples. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 128–142. Springer, Heidelberg (2012)Google Scholar
  22. 22.
    Shved, P., Mandrykin, M., Mutilin, V.: Predicate analysis with Blast 2.7 (Competition contribution). In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 525–527. Springer, Heidelberg (2012)Google Scholar
  23. 23.
    Ströder, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: AProVE: Termination and memory safety of C programs (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 416–418. Springer, Heidelberg (2015)Google Scholar
  24. 24.
    Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: MU-CSeq 0.3: Sequentialization by read-implicit and coarse-grained memory unwindings (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 435–437. Springer, Heidelberg (2015)Google Scholar
  25. 25.
    Urban, C.: FuncTion: An abstract domain functor for termination (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 463–465. Springer, Heidelberg (2015)Google Scholar
  26. 26.
    Wang, W., Barrett, C.: Cascade (Competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 419–421. Springer, Heidelberg (2015)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Dirk Beyer
    • 1
  1. 1.University of PassauPassauGermany

Personalised recommendations