{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T09:35:45Z","timestamp":1758706545500},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T00:00:00Z","timestamp":1439856000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1007\/s10009-015-0396-8","type":"journal-article","created":{"date-parts":[[2015,8,17]],"date-time":"2015-08-17T08:29:47Z","timestamp":1439800187000},"page":"647-657","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["VerifyThis 2012"],"prefix":"10.1007","volume":"17","author":[{"given":"Marieke","family":"Huisman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Klebanov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rosemary","family":"Monahan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,18]]},"reference":[{"key":"396_CR1","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., H\u00e4hnle, 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)","DOI":"10.1007\/978-3-319-12154-3_4"},{"key":"396_CR2","doi-asserted-by":"crossref","unstructured":"Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filli\u00e2tre, J.-C., Grigore, R., Huisman, M., Klebanov, V., March\u00e9, 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)","DOI":"10.1007\/978-3-642-31762-0_2"},{"key":"396_CR3","doi-asserted-by":"crossref","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Let\u2019s verify this with Why3. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)","DOI":"10.1007\/s10009-014-0314-5"},{"key":"396_CR4","doi-asserted-by":"crossref","unstructured":"Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Formal Methods of LNCS, vol. 8442, pp. 127\u2013131. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_9"},{"key":"396_CR5","doi-asserted-by":"crossref","unstructured":"Blom, S., Huisman, M.: Witnessing the elimination of magic wands. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)","DOI":"10.1007\/s10009-015-0372-3"},{"issue":"4","key":"396_CR6","first-page":"1","volume":"4","author":"Dirk Beyer","year":"2014","unstructured":"Beyer, Dirk, Huisman, Marieke, Klebanov, Vladimir, Monahan, Rosemary: Evaluating software verification systems: benchmarks and competitions (Dagstuhl Reports 14171). Dagstuhl Rep 4(4), 1\u201319 (2014)","journal-title":"Dagstuhl Rep"},{"key":"396_CR7","volume-title":"Synthesis of parallel algorithms","author":"E Guy","year":"1993","unstructured":"Guy, E.: Blelloch. Prefix sums and their applications. In: Reif, John H. (ed.) Synthesis of parallel algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1993)"},{"key":"396_CR8","doi-asserted-by":"crossref","unstructured":"Broy, M., Merz, S., Spies, K.: (ed) Formal systems specification. In: The RPC-Memory Specification Case Study of LNCS, vol. 1169. Springer (1996)","DOI":"10.1007\/BFb0024423"},{"key":"396_CR9","unstructured":"Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)"},{"key":"396_CR10","doi-asserted-by":"crossref","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Micha\u0142Moskal, 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 \u201909, pp. 23\u201342. Springer-Verlag (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"396_CR11","unstructured":"Chong, N.: Scalable verification techniques for data-parallel programs. PhD thesis, Imperial College London (2014)"},{"key":"396_CR12","doi-asserted-by":"crossref","unstructured":"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\u201904, pp. 108\u2013128. Springer-Verlag (2005)","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"396_CR13","doi-asserted-by":"crossref","unstructured":"Craigen, D.: Strengths and weaknesses of program verification systems. In: Proceedings of the 1st European Software Engineering Conference on ESEC \u201987, pp. 396\u2013404. Springer-Verlag (1987)","DOI":"10.1007\/BFb0022132"},{"key":"396_CR14","unstructured":"Dross, C., Efstathopoulos, P., Lesens, D., Mentr\u00e9, 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}$$ 2 2014) (2014)"},{"key":"396_CR15","doi-asserted-by":"crossref","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)","DOI":"10.1007\/s10009-014-0308-3"},{"key":"396_CR16","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J.-C., Paskevich, A.: Why3: where programs meet provers. In: Proceedings of the 22nd European Conference on Programming Languages and Systems, ESOP\u201913, pp. 125\u2013128. Springer-Verlag (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"396_CR17","unstructured":"Filli\u00e2tre, 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)"},{"key":"396_CR18","unstructured":"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)"},{"key":"396_CR19","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/s10009-014-0322-5"},{"key":"396_CR20","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"G Huet","year":"1997","unstructured":"Huet, G.: The zipper. J Funct Program 7, 549\u2013554 (1997)","journal-title":"J Funct Program"},{"key":"396_CR21","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F.: Solving the VerifyThis: challenges with VeriFast, p. 2015. J. Softw. Tools Technol. Transfer, (in this issue, Int) (2012)","DOI":"10.1007\/s10009-014-0310-9"},{"key":"396_CR22","doi-asserted-by":"crossref","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, 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\u00df, 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)","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"396_CR23","doi-asserted-by":"crossref","unstructured":"K\u00e4rkk\u00e4inen, J., Sanders, P.: Simple linear work suffix array construction. In: Proceedings of the 30th International Conference on Automata, languages and programming, ICALP\u201903, pp. 943\u2013955, Berlin, Heidelberg, Springer-Verlag (2003)","DOI":"10.1007\/3-540-45061-0_73"},{"key":"396_CR24","doi-asserted-by":"crossref","unstructured":"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\u201910, pp. 348\u2013370. Springer-Verlag (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"396_CR25","doi-asserted-by":"crossref","unstructured":"Lewerentz, C., Lindner, T.: Case study \u201cproduction cell\u201d: 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\u2013416. Springer (1995)","DOI":"10.1007\/BFb0015473"},{"key":"396_CR26","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"Gary T Leavens","year":"2007","unstructured":"Leavens, Gary T., Leino, K.Rustan M., M\u00fcller, Peter: Specification and verification challenges for sequential object-oriented programs. Form. Asp. Comput. 19, 159\u2013189 (2007)","journal-title":"Form. Asp. Comput."},{"key":"396_CR27","unstructured":"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)"},{"key":"396_CR28","doi-asserted-by":"crossref","unstructured":"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\u201910, pp. 371\u2013377. Springer-Verlag (2010)","DOI":"10.1007\/978-3-642-15643-4_30"},{"key":"396_CR29","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.scico.2013.01.006","volume":"82","author":"P Philippaerts","year":"2014","unstructured":"Philippaerts, P., M\u00fchlberg, J.Tobias, Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with verifast. Sci. Comput. Program. 82, 77\u201397 (2014)","journal-title":"Sci. Comput. Program."},{"key":"396_CR30","doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Wolfgang, B., Peter H.S. (eds) Automated deduction\u2014a basis for applications of applied logic series, vol. 9 , pp. 13\u201339. Springer, Netherlands (1998)","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"396_CR31","volume-title":"Algorithms","author":"R Sedgewick","year":"2011","unstructured":"Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, USA (2011)","edition":"4"},{"key":"396_CR32","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Martin, N.: AutoProof meets some verification challenges. Int. J. Softw. Tools Technol. Transfer (in this issue) (2015)","DOI":"10.1007\/s10009-014-0300-y"},{"key":"396_CR33","unstructured":"Tuerk, T.: Local reasoning about while-loops. In: M\u00fcller, P., Naumann, D., Yang, H. (eds) Proceedings VS-Theory Workshop of VSTTE, pp. 29\u201339 (2010)"},{"issue":"10","key":"396_CR34","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the verified software grand challenge. Computer 39(10), 57\u201364 (2006)","journal-title":"Computer"},{"key":"396_CR35","doi-asserted-by":"crossref","unstructured":"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\u201398. Springer (2008)","DOI":"10.1007\/978-3-540-87873-5_10"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0396-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0396-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0396-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,29]],"date-time":"2019-08-29T12:21:45Z","timestamp":1567081305000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0396-8"}},"subtitle":["A Program Verification Competition"],"short-title":[],"issued":{"date-parts":[[2015,8,18]]},"references-count":35,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["396"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0396-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,18]]}}}