{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T04:04:28Z","timestamp":1750910668425,"version":"3.41.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031676949"},{"type":"electronic","value":"9783031676956"}],"license":[{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-67695-6_6","type":"book-chapter","created":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T14:03:04Z","timestamp":1730383384000},"page":"160-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The VerifyThis Collaborative Long-Term Challenge Series"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Ahrendt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paula","family":"Herber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ra\u00fal E.","family":"Monti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Weigl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,1]]},"reference":[{"key":"6_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-19849-6_1","volume-title":"ISoLA 2022","author":"W Ahrendt","year":"2022","unstructured":"Ahrendt, W., Herber, P., Huisman, M., Ulbrich, M.: SpecifyThis - bridging gaps between program specification paradigms. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13701, pp. 3\u20136. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_1"},{"key":"6_CR2","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-031-19849-6_2","volume-title":"ISoLA 2022","author":"J Amilon","year":"2022","unstructured":"Amilon, J., Lidstr\u00f6m, C., Gurov, D.: Deductive verification based abstraction for software model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13701, pp. 7\u201328. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_2"},{"key":"6_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-031-47705-8_9","volume-title":"iFM 2023","author":"L Armborst","year":"2023","unstructured":"Armborst, L., Lathouwers, S., Huisman, M.: Joining forces! Reusing contracts for deductive verifiers through automatic translation. In: Herber, P., Wijs, A. (eds.) iFM 2023. LNCS, vol. 14300, pp. 153\u2013171. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_9"},{"key":"6_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). http:\/\/smtlib.cs.uiowa.edu\/language.shtml"},{"key":"6_CR5","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language. http:\/\/frama-c.com\/download\/acsl.pdf"},{"key":"6_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-031-30820-8_29","volume-title":"TACAS 2023","author":"D Beyer","year":"2023","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 495\u2013522. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29"},{"key":"6_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-031-17108-6_7","volume-title":"SEFM 2022","author":"D Beyer","year":"2022","unstructured":"Beyer, D., Spiessl, M., Umbricht, S.: Cooperation between automatic and interactive software verifiers. In: Schlingloff, B.H., Chai, M. (eds.) SEFM 2022. LNCS, vol. 13550, pp. 111\u2013128. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_7"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-030-17502-3_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Ernst","year":"2019","unstructured":"Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: VerifyThis \u2013 verification competition with a human factor. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 176\u2013195. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_12"},{"key":"6_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-031-19849-6_4","volume-title":"ISoLA 2022","author":"G Ernst","year":"2022","unstructured":"Ernst, G., Knapp, A., Murray, T.: A Hoare logic with regular behavioral specifications. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13701, pp. 45\u201364. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_4"},{"key":"6_CR10","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-47705-8_5","volume-title":"iFM 2023","author":"G Ernst","year":"2023","unstructured":"Ernst, G., Weigl, A.: Verify This: memcached\u2013a practical long-term challenge for the integration of formal methods. In: Herber, P., Wijs, A. (eds.) iFM 2023. LNCS, vol. 14300. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_5"},{"key":"6_CR11","unstructured":"Ernst, G., Weigl, A.: VerifyThis Long-term Challenge: Specifying and Verifying a Real-life Remote Key-Value Cache (memcached) (2023). https:\/\/verifythis.github.io\/03memcached\/challenge.pdf"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Gurov, D., H\u00e4hnle, R., Huisman, M., Reger, G., Lidstr\u00f6m, C.: Principles of Contract Languages (Dagstuhl Seminar 22451). Dagstuhl Reports, vol. 12, no. 11, pp. 1\u201327 (2023). https:\/\/doi.org\/10.4230\/DagRep.12.11.1","DOI":"10.4230\/DagRep.12.11.1"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science","author":"R H\u00e4hnle","year":"2019","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18"},{"issue":"1","key":"6_CR14","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"CAR Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler: a grand challenge for computing research. J. ACM 50(1), 63\u201369 (2003). https:\/\/doi.org\/10.1145\/602382.602403","journal-title":"J. ACM"},{"key":"6_CR15","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: On the organisation of program verification competitions. In: COMPARE. CEUR Workshop Proceedings, vol.\u00a0873, pp. 50\u201359 (2012). https:\/\/ceur-ws.org\/Vol-873\/papers\/paper_2.pdf"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-030-64354-6_10","volume-title":"Deductive Software Verification: Future Perspectives","author":"M Huisman","year":"2020","unstructured":"Huisman, M., Monti, R., Ulbrich, M., Weigl, A.: The VerifyThis collaborative long term challenge. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.) Deductive Software Verification: Future Perspectives. LNCS, vol. 12345, pp. 246\u2013260. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_10"},{"issue":"2","key":"6_CR17","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/s00165-006-0022-3","volume":"19","author":"R Joshi","year":"2007","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Formal Asp. Comput. 19(2), 269\u2013272 (2007). https:\/\/doi.org\/10.1007\/s00165-006-0022-3","journal-title":"Formal Asp. Comput."},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V Klebanov","year":"2011","unstructured":"Klebanov, V., et al.: The 1st verified software competition: experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154\u2013168. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_14"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Lanzinger, F., Weigl, A., Ulbrich, M., Dietl, W.: Scalability and precision by combining expressive type systems and deductive verification. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3485520","DOI":"10.1145\/3485520"},{"key":"6_CR20","unstructured":"Leavens, G.T., et al.: JML reference manual (2008)"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Huismann, M., Monti, R.E., Ulbrich, M., Weigl, A. (eds.): VerifyThis Long-term Challenge 2020: Proceedings of the Online-Event (2020). https:\/\/doi.org\/10.5445\/IR\/1000119426","DOI":"10.5445\/IR\/1000119426"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-030-39322-9_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"W Oortwijn","year":"2020","unstructured":"Oortwijn, W., Gurov, D., Huisman, M.: Practical abstractions for automated verification of shared-memory concurrency. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 401\u2013425. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_19"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Sprenger, C., et al.: Igloo: soundly linking compositional refinement and separation logic for distributed system verification. Proc. ACM Program. Lang. 4(OOPSLA), 152:1\u2013152:31 (2020). https:\/\/doi.org\/10.1145\/3428220","DOI":"10.1145\/3428220"},{"key":"6_CR24","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse: Specification, Refinement and Proof. Technical report PRG-126, Oxford University Computing Laboratory (2000). https:\/\/kar.kent.ac.uk\/22009\/1\/An_Electronic_Purse_Specification,_Refinement_and_Proof.pdf"}],"container-title":["Lecture Notes in Computer Science","TOOLympics Challenge 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-67695-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:13:09Z","timestamp":1750842789000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-67695-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,1]]},"ISBN":["9783031676949","9783031676956"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-67695-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,1]]},"assertion":[{"value":"1 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}