[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

VerifyThis 2012

A Program Verification Competition

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

Abstract

VerifyThis 2012 was a 2-day verification competition that took place as part of the International Symposium on Formal Methods (FM 2012) on August 30–31, 2012, in Paris, France. It was the second installment in the VerifyThis series. After the competition, an open call solicited contributions related to the VerifyThis 2012 challenges and overall goals. As a result, seven papers were submitted and, after review and revision, included in this special issue. In this introduction to the special issue, we provide an overview of the VerifyThis competition series, an account of related activities in the area, and an overview of solutions submitted to the organizers both during and after the 2012 competition. We conclude with a summary of results and some remarks concerning future installments of VerifyThis.

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
$34.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 excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1

Similar content being viewed by others

Notes

  1. http://www.satcompetition.org, http://www.smtcomp.org, http://ipc.icaps-conference.org, http://www.qbflib.org/competition.html, http://fmv.jku.at/hwmcc11, http://sv-comp.sosy-lab.org, and http://www.cs.miami.edu/~tptp/CASC.

  2. In particular, because the author of the best challenge submission was participating in the competition.

  3. http://www.verifythis.org.

  4. http://www.vscomp.org.

  5. http://sv-comp.sosy-lab.org.

  6. http://rers-challenge.org.

  7. The challenge can be found in the SV-COMP database at https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c/heap-manipulation/bubble_sort_linux_false-unreach-call.c.

  8. Available as part of the original challenge http://fm2012.verifythis.org and in Appendix 6.

  9. The original challenge description contained an illustrating excerpt from a slide deck on prefix sums.

  10. AutoProof has been significantly improved since its 2013 version used here.

  11. This specification uses a loop contract. If the tool supported contracts for arbitrary code blocks, then the modification after the loop could be included and a simpler solution as proposed by Tuerk would have been possible.

References

  1. Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., Hähnle, R., Hentschel, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P.H., Ulbrich, M.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D., Polgreen, E., Shankar, N., (eds) Proceedings, 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), Vienna, July 2014, LNCS. Springer (2014)

  2. Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filliâtre, J.-C., Grigore, R., Huisman, M., Klebanov, V., Marché, C., Monahan, R., Mostowski, W., Polikarpova, N., Scheben, C., Schellhorn, G., Tofan, B., Tschannen, J., Ulbrich, M.: The COST IC0701 verification competition 2011. In: Beckert, B., Damiani, F., Gurov, D., (eds) International Conference on Formal Verification of Object-Oriented Systems (FoVeOOS 2011), LNCS. Springer (2012)

  3. Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Let’s verify this with Why3. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)

  4. Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Formal Methods of LNCS, vol. 8442, pp. 127–131. Springer (2014)

  5. Blom, S., Huisman, M.: Witnessing the elimination of magic wands. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)

  6. Beyer, Dirk, Huisman, Marieke, Klebanov, Vladimir, Monahan, Rosemary: Evaluating software verification systems: benchmarks and competitions (Dagstuhl Reports 14171). Dagstuhl Rep 4(4), 1–19 (2014)

    Google Scholar 

  7. Guy, E.: Blelloch. Prefix sums and their applications. In: Reif, John H. (ed.) Synthesis of parallel algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1993)

    Google Scholar 

  8. Broy, M., Merz, S., Spies, K.: (ed) Formal systems specification. In: The RPC-Memory Specification Case Study of LNCS, vol. 1169. Springer (1996)

  9. Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)

  10. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., MichałMoskal, S., Thomas, S., Wolfram, T.S.: VCC: a practical system for verifying concurrent C. In: Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’09, pp. 23–42. Springer-Verlag (2009)

  11. Chong, N.: Scalable verification techniques for data-parallel programs. PhD thesis, Imperial College London (2014)

  12. Cok, D.R., Kiniry, J.R.: Esc/java2: Uniting ESC/Java and JML. In: Proceedings of the 2004 International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS’04, pp. 108–128. Springer-Verlag (2005)

  13. Craigen, D.: Strengths and weaknesses of program verification systems. In: Proceedings of the 1st European Software Engineering Conference on ESEC ’87, pp. 396–404. Springer-Verlag (1987)

  14. Dross, C., Efstathopoulos, P., Lesens, D., Mentré, D., Moy, Y.: Rail, space, security: Three case studies for SPARK 2014. In: 7th Europen Congress on Embedded Real Time Software and Systems (ERTS\(^{2}\) 2014) (2014)

  15. Ernst, G., Pfähler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)

  16. Filliâtre J.-C., Paskevich, A.: Why3: where programs meet provers. In: Proceedings of the 22nd European Conference on Programming Languages and Systems, ESOP’13, pp. 125–128. Springer-Verlag (2013)

  17. Filliâtre, J.-C, Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Klebanov, V., Biere, A., Beckert, B., Sutcliffe, G. (eds) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012) (2012)

  18. Huisman, M., Klebanov, V., Monahan, R.: On the organisation of program verification competitions. In: Vladimir, K., Bernhard, B., Biere A., Sutcliffe, G. (eds) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE), Manchester, UK, June 30, 2012, of CEUR Workshop Proceedings. vol. 873, CEUR-WS.org (2012)

  19. Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: SPARK 2014 and GNATprove. A competition report from builders of an industrial-strength verifying compiler. Int. J. Softw. Tools Technol. (Transfer, in this issue) (2015)

  20. Huet, G.: The zipper. J Funct Program 7, 549–554 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  21. Jacobs, B., Smans, J., Piessens, F.: Solving the VerifyThis: challenges with VeriFast, p. 2015. J. Softw. Tools Technol. Transfer, (in this issue, Int) (2012)

  22. Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Weiß, B.: The 1st verified software competition: experience report. In: Michael, B., Wolfram, S., (eds) Proceedings, 17th International Symposium on Formal Methods (FM) of LNCS, vol. 6664. Springer (2011)

  23. Kärkkäinen, J., Sanders, P.: Simple linear work suffix array construction. In: Proceedings of the 30th International Conference on Automata, languages and programming, ICALP’03, pp. 943–955, Berlin, Heidelberg, Springer-Verlag (2003)

  24. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’10, pp. 348–370. Springer-Verlag (2010)

  25. Lewerentz, C., Lindner, T.: Case study “production cell”: a comparative study in formal specification and verification. In: Manfred, B., Stefan, J., (eds) KORSO: Methods, Languages, and Tools for the Construction of Correct Software of LNCS, vol. 1009, pp. 388–416. Springer (1995)

  26. Leavens, Gary T., Leino, K.Rustan M., Müller, Peter: Specification and verification challenges for sequential object-oriented programs. Form. Asp. Comput. 19, 159–189 (2007)

    Article  MATH  Google Scholar 

  27. Leino, K.R.M., Moskal, M.: VACID-0: verification of ample correctness of invariants of data-structures, edn 0. In: Proceedings of Tools and Experiments Workshop at VSTTE (2010)

  28. Liu, Y., Sun, J., Dong, J.S.: Developing model checkers using PAT. In: Proceedings of the 8th International Conference on Automated Technology for Verification and Analysis, ATVA’10, pp. 371–377. Springer-Verlag (2010)

  29. Philippaerts, P., Mühlberg, J.Tobias, Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with verifast. Sci. Comput. Program. 82, 77–97 (2014)

    Article  Google Scholar 

  30. Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Wolfgang, B., Peter H.S. (eds) Automated deduction—a basis for applications of applied logic series, vol. 9 , pp. 13–39. Springer, Netherlands (1998)

  31. Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, USA (2011)

    Google Scholar 

  32. Tschannen, J., Furia, C.A., Martin, N.: AutoProof meets some verification challenges. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)

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

  34. Woodcock, J.: First steps in the verified software grand challenge. Computer 39(10), 57–64 (2006)

    Article  Google Scholar 

  35. Weide, B.W., Sitaraman, M., Harton, H.K., Adcock, B.M., Bucci, P., Bronish, D., Heym, W.D., Kirschenbaum, J., Frazier, D.: Incremental benchmarks for software verification tools and techniques. In: Shankar, N., Woodcock, J. (eds) Proceedings verified software: theories, tools, experiments (VSTTE) of LNCS, vol. 5295, pp. 84–98. Springer (2008)

Download references

Acknowledgments

The organizers would like to thank Rustan Leino, Nadia Polikarpova, and Mattias Ulbrich for their feedback and support prior to the competition.

Author information

Authors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Marieke Huisman

  2. Karlsruhe Institute of Technology, Karlsruhe, Germany

    Vladimir Klebanov

  3. Maynooth University, Maynooth, Co. Kildare, Ireland

    Rosemary Monahan

Authors
  1. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vladimir Klebanov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rosemary Monahan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rosemary Monahan.

Appendices

LCP/LRS source code

figure f
figure g

PrefixSum source code

1.1 Recursive version

figure h

1.2 Iterative version

figure i

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Huisman, M., Klebanov, V. & Monahan, R. VerifyThis 2012. Int J Softw Tools Technol Transfer 17, 647–657 (2015). https://doi.org/10.1007/s10009-015-0396-8

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-015-0396-8

Keywords

Search

Navigation