{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T11:02:00Z","timestamp":1761562920248,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031198489"},{"type":"electronic","value":"9783031198496"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19849-6_11","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T15:03:32Z","timestamp":1666191812000},"page":"174-187","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["TriCo\u2014Triple Co-piloting of\u00a0Implementation, Specification and\u00a0Tests"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5671-2555","authenticated-orcid":false,"given":"Wolfgang","family":"Ahrendt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0074-8786","authenticated-orcid":false,"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1097-8278","authenticated-orcid":false,"given":"Moa","family":"Johansson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2733-7098","authenticated-orcid":false,"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"11_CR1","unstructured":"Codemirror. https:\/\/codemirror.net"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification-The KeY Book","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification-The KeY Book. LNCS, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-319-49812-6_12","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"W Ahrendt","year":"2016","unstructured":"Ahrendt, W., Gladisch, C., Herda, M.: Proof-based test case generation. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P., Ulbrich, M. (eds.) Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 415\u2013451. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_12"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. In: Proceedings of POPL, vol. 51. ACM (2016)","DOI":"10.1145\/2837614.2837628"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-030-64354-6_6","volume-title":"Deductive Software Verification: Future Perspectives","author":"A Alshnakat","year":"2020","unstructured":"Alshnakat, A., Gurov, D., Lidstr\u00f6m, C., R\u00fcmmer, P.: Constraint-based contract inference for deductive verification. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.) Deductive Software Verification: Future Perspectives. LNCS, vol. 12345, pp. 149\u2013176. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_6"},{"key":"11_CR6","unstructured":"Austin, J., et al.: Program synthesis with large language models (2021). arXiv:2108.07732"},{"issue":"6","key":"11_CR7","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/1953122.1953145","volume":"54","author":"M Barnett","year":"2011","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81\u201391 (2011)","journal-title":"Commun. ACM"},{"key":"11_CR8","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:\/\/www.smt-lib.org\/"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"11_CR10","unstructured":"Chen, M., et al.: Evaluating large language models trained on code, arxiv:2107.03374 (2021). arXiv:2107.03374"},{"key":"11_CR11","unstructured":"Chowdhery, A., et al.: PaLM: scaling language modeling with pathways (2022). arXiv:2204.02311"},{"issue":"1\u20133","key":"11_CR12","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., et al.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., R\u00fcmmer, P.: Competition report: CHC-COMP-21. In: Hojjat, H., Kafle, B. (eds.) Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2021, Virtual, 28 March 2021. EPTCS, vol. 344, pp. 91\u2013108 (2021)","DOI":"10.4204\/EPTCS.344.7"},{"issue":"6","key":"11_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3357231","volume":"52","author":"M Gleirscher","year":"2019","unstructured":"Gleirscher, M., Foster, S., Woodcock, J.: New opportunities for integrated formal methods. ACM Comput. Surv. (CSUR) 52(6), 1\u201336 (2019)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-1-84882-912-1_5","volume-title":"Reflections on the Work of C.A.R. Hoare","author":"M Gordon","year":"2010","unstructured":"Gordon, M., Collavizza, H.: Forward with Hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, pp. 101\u2013121. Springer, London (2010). https:\/\/doi.org\/10.1007\/978-1-84882-912-1_5"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-17685-2_6","volume-title":"Central European Functional Programming School","author":"J Hughes","year":"2010","unstructured":"Hughes, J.: Software testing with QuickCheck. In: Horv\u00e1th, Z., Plasmeijer, R., Zs\u00f3k, V. (eds.) CEFP 2009. LNCS, vol. 6299, pp. 183\u2013223. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17685-2_6"},{"issue":"1","key":"11_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2071356.2071363","volume":"17","author":"C Ioannides","year":"2012","unstructured":"Ioannides, C., Eder, K.I.: Coverage-directed test generation automated by machine learning - a review. ACM Trans. Des. Autom. Electron. Syst. 17(1), 1\u201321 (2012)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"issue":"4","key":"11_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 1\u201354 (2009)","journal-title":"ACM Comput. Surv."},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-38916-0_10","volume-title":"Tests and Proofs","author":"N Kosmatov","year":"2013","unstructured":"Kosmatov, N., Prevosto, V., Signoles, J.: A lesson on proof of programs with Frama-C. Invited tutorial paper. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 168\u2013177. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38916-0_10"},{"key":"11_CR20","volume-title":"Agile Software Development: Principles, Patterns, and Practices","author":"RC Martin","year":"2003","unstructured":"Martin, R.C.: Agile Software Development: Principles, Patterns, and Practices. Prentice Hall PTR, Hoboken (2003)"},{"key":"11_CR21","unstructured":"Parthasarathy, M., Garg, P.: Machine-learning based methods for synthesizing invariants. Tutorial at CAV 2015 (2015)"},{"issue":"1","key":"11_CR22","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s10515-020-00270-x","volume":"27","author":"C Richter","year":"2020","unstructured":"Richter, C., H\u00fcllermeier, E., Jakobs, M., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Autom. Softw. Eng. 27(1), 153\u2013186 (2020)","journal-title":"Autom. Softw. Eng."},{"key":"11_CR23","unstructured":"Seghir, M.N., Kroening, D.: Counterexample-guided precondition inference. In: Proceedings of Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, 16\u201324 March 2013, pp. 451\u2013471 (2013)"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: Cute: a concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC\/FSE-13, pp. 263\u2013272. Association for Computing Machinery, New York (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"11_CR25","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Advances in Neural Information Processing Systems 31, NeurIPS 2018, Montr\u00e9al, Canada (2018). https:\/\/proceedings.neurips.cc\/paper\/2018"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-81688-9_6","volume-title":"Computer Aided Verification","author":"E Singher","year":"2021","unstructured":"Singher, E., Itzhaky, S.: Theory exploration powered by deductive synthesis. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 125\u2013148. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_6"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Smallbone, N., Johannson, M., Claessen, K., Algehed, M.: Quick specifications for the busy programmer. J. Funct. Program. 27 (2017)","DOI":"10.1017\/S0956796817000090"},{"issue":"1","key":"11_CR28","first-page":"137","volume":"64","author":"H Takeuchi","year":"1986","unstructured":"Takeuchi, H., Nonaka, I.: The new new product development game. Harv. Bus. Rev. 64(1), 137\u2013146 (1986)","journal-title":"Harv. Bus. Rev."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19849-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:08:25Z","timestamp":1666224505000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19849-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031198489","9783031198496"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19849-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}