{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:37Z","timestamp":1775873677768,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030643539","type":"print"},{"value":"9783030643546","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-64354-6_6","type":"book-chapter","created":{"date-parts":[[2020,12,8]],"date-time":"2020-12-08T09:12:03Z","timestamp":1607418723000},"page":"149-176","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Constraint-Based Contract Inference for Deductive Verification"],"prefix":"10.1007","author":[{"given":"Anoud","family":"Alshnakat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Lidstr\u00f6m","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":[[2020,12,4]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 789\u2013801. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837628","DOI":"10.1145\/2837614.2837628"},{"key":"6_CR3","unstructured":"Alshnakat, A.: Automatic verification of embedded systems using horn clause solvers. Master\u2019s thesis, Uppsala University, Department of Information Technology (2019)"},{"issue":"2\u20133","key":"6_CR4","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2\u20133), 124\u2013400 (2018)","journal-title":"Found. Trends Electron. Des. Autom."},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_31"},{"key":"6_CR6","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":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-13977-2_3","volume-title":"Tests and Proofs","author":"K Claessen","year":"2010","unstructured":"Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 6\u201321. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13977-2_3"},{"key":"6_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"6_CR10","unstructured":"Danial, A.: Cloc - count lines of code. http:\/\/cloc.sourceforge.net\/"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Denney, E., Fischer, B.: A generic annotation inference algorithm for the safety certification of automatically generated code. In: Jarzabek, S., Schmidt, D.C., Veldhuizen, T.L. (eds.) Generative Programming and Component Engineering, 5th International Conference, GPCE 2006, Portland, Oregon, USA, 22\u201326 October 2006, Proceedings, pp. 121\u2013130. ACM (2006), https:\/\/doi.org\/10.1145\/1173706.1173725","DOI":"10.1145\/1173706.1173725"},{"issue":"8","key":"6_CR12","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, non determinacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). http:\/\/doi.acm.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"key":"6_CR13","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976). http:\/\/www.worldcat.org\/oclc\/01958445"},{"issue":"1\u20133","key":"6_CR14","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). https:\/\/doi.org\/10.1016\/j.scico.2007.01.015","journal-title":"Sci. Comput. Program."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","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. LNCS, pp. 101\u2013121. Springer, London (2010). https:\/\/doi.org\/10.1007\/978-1-84882-912-1_5"},{"key":"6_CR16","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416 (2012). http:\/\/doi.acm.org\/10.1145\/2254064.2254112"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Comput. Aided Verif.","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). http:\/\/doi.acm.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, 30 October\u20132 November 2018. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P., Subotic, P., Yi, W.: Horn clauses for communicating timed systems. In: Bj\u00f8rner, N., Fioravanti, F., Rybalchenko, A., Senni, V. (eds.) Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014. EPTCS, vol. 169, pp. 39\u201352 (2014). https:\/\/doi.org\/10.4204\/EPTCS.169.6","DOI":"10.4204\/EPTCS.169.6"},{"issue":"5","key":"6_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"6_CR22","unstructured":"Jones, C.B.: Developing methods for computer programs including a notion of interference. Ph.D. thesis, University of Oxford, UK (1981). http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.259064"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-319-41528-4_19","volume-title":"Computer Aided Verification","author":"T Kahsai","year":"2016","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-030-03427-6_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"A Kn\u00fcppel","year":"2018","unstructured":"Kn\u00fcppel, A., Th\u00fcm, T., Padylla, C., Schaefer, I.: Scalability of deductive verification depends on method call treatment. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 159\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_15"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2"},{"issue":"10","key":"6_CR26","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Comput. 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","journal-title":"IEEE Comput."},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78163-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y Moy","year":"2008","unstructured":"Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 188\u2013202. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_18"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-030-03427-6_14","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"M Nyberg","year":"2018","unstructured":"Nyberg, M., Gurov, D., Lidstr\u00f6m, C., Rasmusson, A., Westman, J.: Formal verification in automotive industry: enablers and obstacles. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 139\u2013158. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_14"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-46691-6_13","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"D Oheimb","year":"1999","unstructured":"Oheimb, D.: Hoare logic for mutual recursion and local variables. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 168\u2013180. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-46691-6_13"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-319-66845-1_17","volume-title":"Integrated Formal Methods","author":"O Owe","year":"2017","unstructured":"Owe, O., Ramezanifarkhani, T., Fazeldehkordi, E.: Hoare-style reasoning from multiple contracts. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 263\u2013278. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_17"},{"key":"6_CR31","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf. 6, 319\u2013340 (1976). https:\/\/doi.org\/10.1007\/BF00268134","journal-title":"Acta Inf."},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Polikarpova, N., Ciupa, I., Meyer, B.: A comparative study of programmer-written and automatically inferred contracts. In: Rothermel, G., Dillon, L.K. (eds.) Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, ISSTA 2009, Chicago, IL, USA, 19\u201323 July 2009, pp. 93\u2013104. ACM (2009). https:\/\/doi.org\/10.1145\/1572272.1572284","DOI":"10.1145\/1572272.1572284"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-642-37036-6_25","volume-title":"Programming Languages and Systems","author":"MN Seghir","year":"2013","unstructured":"Seghir, M.N., Kroening, D.: Counterexample-guided precondition inference. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 451\u2013471. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_25"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-12736-1_13","volume-title":"Programming Languages and Systems","author":"MN Seghir","year":"2014","unstructured":"Seghir, M.N., Schrammel, P.: Necessary and sufficient preconditions via eager abstraction. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 236\u2013254. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12736-1_13"},{"key":"6_CR36","unstructured":"Singleton, J.L., Leavens, G.T., Rajan, H., Cok, D.R.: Inferring concise specifications of APIs. CoRR abs\/1905.06847 (2019). http:\/\/arxiv.org\/abs\/1905.06847"},{"key":"6_CR37","unstructured":"SV-Comp: Collection of verification tasks. https:\/\/github.com\/sosy-lab\/sv-benchmarks"}],"container-title":["Lecture Notes in Computer Science","Deductive Software Verification: Future Perspectives"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-64354-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,8]],"date-time":"2020-12-08T09:20:07Z","timestamp":1607419207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-64354-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030643539","9783030643546"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-64354-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"4 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}