{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:26:33Z","timestamp":1750843593512,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031477041"},{"type":"electronic","value":"9783031477058"}],"license":[{"start":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T00:00:00Z","timestamp":1699228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T00:00:00Z","timestamp":1699228800000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-47705-8_5","type":"book-chapter","created":{"date-parts":[[2023,11,10]],"date-time":"2023-11-10T09:02:24Z","timestamp":1699606944000},"page":"82-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verify\u00a0This: Memcached\u2014A Practical Long-Term Challenge for\u00a0the\u00a0Integration of\u00a0Formal Methods"],"prefix":"10.1007","author":[{"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Weigl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,11,6]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Herber, P., Huisman, M., Ulbrich, M.: SpecifyThis - bridging gaps between program specification paradigms. In: ISoLA (1). LNCS, vol. 13701, pp. 3\u20136. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_1","DOI":"10.1007\/978-3-031-19849-6_1"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: TACAS (2). LNCS, vol. 13994, pp. 495\u2013522. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Software testing: 5th comparative evaluation: Test-Comp 2023. In: FASE. LNCS, vol. 13991, pp. 309\u2013323. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_17","DOI":"10.1007\/978-3-031-30826-0_17"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-030-61362-4_8","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"D Beyer","year":"2020","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: survey and unifying component framework. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 143\u2013167. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"issue":"4","key":"5_CR6","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1002\/spe.2949","volume":"51","author":"N Chong","year":"2021","unstructured":"Chong, N., et al.: Code-level model checking in the software development workflow at Amazon Web Services. Softw. Pract. Exp. 51(4), 772\u2013797 (2021)","journal-title":"Softw. Pract. Exp."},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"Computer Aided Verification","author":"A Chudnov","year":"2018","unstructured":"Chudnov, A., et al.: Continuous formal verification of amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26"},{"key":"5_CR8","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model checking, 2nd edn. MIT Press (2018)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: JML and OpenJML for Java 16. In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs, pp. 65\u201367 (2021)","DOI":"10.1145\/3464971.3468417"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-35873-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Cruanes","year":"2013","unstructured":"Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 275\u2013294. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_18"},{"issue":"8","key":"5_CR11","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/3338112","volume":"62","author":"D Distefano","year":"2019","unstructured":"Distefano, D., F\u00e4hndrich, M., Logozzo, F., O\u2019Hearn, P.W.: Scaling static analyses at Facebook. Commun. ACM 62(8), 62\u201370 (2019)","journal-title":"Commun. ACM"},{"key":"5_CR12","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":"5_CR13","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":"5_CR14","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., R\u00fcmmer, P.: Competition report: CHC-COMP-21. arXiv preprint arXiv:2109.04635 (2021)","DOI":"10.4204\/EPTCS.344.7"},{"key":"5_CR15","unstructured":"Filli\u00e2tre, J., Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Klebanov, V., Beckert, B., Biere, A., Sutcliffe, G. (eds.) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, 30 June 2012. CEUR Workshop Proceedings, vol. 873, pp. 36\u201349. CEUR-WS.org (2012)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Computing and Software Science: State of the Art and Perspectives, pp. 345\u2013373 (2019)","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-030-61362-4_29","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"B Jacobs","year":"2020","unstructured":"Jacobs, B.: Modular verification of liveness properties of the I\/O behavior of imperative programs. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 509\u2013524. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_29"},{"key":"5_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"},{"issue":"6","key":"5_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-030-99524-9_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JR Koenig","year":"2022","unstructured":"Koenig, J.R., Padon, O., Shoham, S., Aiken, A.: Inferring invariants with quantifier alternations: taming the search space explosion. In: TACAS 2022. LNCS, vol. 13243, pp. 338\u2013356. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_18"},{"issue":"7","key":"5_CR21","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Continuous reasoning: scaling the impact of formal methods. In: Proceedings of the 33rd annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 13\u201325 (2018)","DOI":"10.1145\/3209108.3209109"},{"issue":"11","key":"5_CR23","doi-asserted-by":"publisher","first-page":"3928","DOI":"10.3390\/app10113928","volume":"10","author":"W Oortwijn","year":"2020","unstructured":"Oortwijn, W., Gurov, D., Huisman, M.: An abstraction technique for verifying shared-memory concurrency. Appl. Sci. 10(11), 3928 (2020)","journal-title":"Appl. Sci."},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Sprenger, C., et al.: Igloo: soundly linking compositional refinement and separation logic for distributed system verification. In: Proceedings of the ACM on Programming Languages 4(OOPSLA), pp. 1\u201331 (2020)","DOI":"10.1145\/3428220"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47705-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,18]],"date-time":"2024-04-18T14:51:55Z","timestamp":1713451915000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47705-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,6]]},"ISBN":["9783031477041","9783031477058"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47705-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023,11,6]]},"assertion":[{"value":"6 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"iFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Leiden","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/liacs.leidenuniv.nl\/~bonsanguemm\/ifm23\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"51","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}