{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:44:55Z","timestamp":1743043495242,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631387"},{"type":"electronic","value":"9783319631394"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-63139-4_11","type":"book-chapter","created":{"date-parts":[[2017,7,23]],"date-time":"2017-07-23T23:22:55Z","timestamp":1500852175000},"page":"187-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Abstract Contract Synthesis in a Rewriting Framework"],"prefix":"10.1007","author":[{"given":"Mar\u00eda","family":"Alpuente","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Pardo","sequence":"additional","affiliation":[]},{"given":"Alicia","family":"Villanueva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Alpuente, M., Feli\u00fa, M.A., Villanueva, A.: Automatic inference of specifications using matching logic. In: Proceedings of PEPM 2013, pp. 127\u2013136. ACM (2013)","DOI":"10.1145\/2426890.2426914"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.200.1","volume":"200","author":"M Alpuente","year":"2015","unstructured":"Alpuente, M., Pardo, D., Villanueva, A.: Automatic inference of specifications in the K framework. EPTCS 200, 1\u201317 (2015)","journal-title":"EPTCS"},{"issue":"1","key":"11_CR3","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10009-008-0090-1","volume":"11","author":"S Anand","year":"2008","unstructured":"Anand, S., P\u0103s\u0103reanu, C.S., Visser, W.: Symbolic execution with abstraction. STTT 11(1), 53\u201367 (2008)","journal-title":"STTT"},{"issue":"Part A","key":"11_CR4","first-page":"48","volume":"44","author":"A Arusoaie","year":"2015","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V.: Symbolic execution based on language transformation. Comput. Lang. Syst. Struct. 44(Part A), 48\u201371 (2015)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-540-74061-2_25","volume-title":"Static Analysis","author":"C Calcagno","year":"2007","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Footprint analysis: a shape analysis that discovers preconditions. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 402\u2013418. Springer, Heidelberg (2007). doi:\n                      10.1007\/978-3-540-74061-2_25"},{"key":"11_CR6","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). doi:\n                      10.1007\/978-3-642-13977-2_3"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-35873-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128\u2013148. Springer, Heidelberg (2013). doi:\n                      10.1007\/978-3-642-35873-9_10"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: Proceedings of POPL 2012, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103621.2103719"},{"issue":"5","key":"11_CR9","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/2039346.2039349","volume":"33","author":"BS Gulavani","year":"2011","unstructured":"Gulavani, B.S., Chakraborty, S., Ramalingam, G., Nori, A.V.: Bottom-up shape analysis using LISF. ACM Trans. Program. Lang. Syst. 33(5), 17 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-540-45070-2_19","volume-title":"ECOOP 2003 \u2013 Object-Oriented Programming","author":"J Henkel","year":"2003","unstructured":"Henkel, J., Diwan, A.: Discovering algebraic specifications from Java classes. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 431\u2013456. Springer, Heidelberg (2003). doi:\n                      10.1007\/978-3-540-45070-2_19"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0102s\u0102reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553\u2013568. Springer, Heidelberg (2003). doi:\n                      10.1007\/3-540-36577-X_40"},{"issue":"7","key":"11_CR12","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Comm. ACM 19(7), 385\u2013394 (1976)","journal-title":"Comm. ACM"},{"key":"11_CR13","volume-title":"Abstraction and Specification in Program Development","author":"B Liskov","year":"1986","unstructured":"Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)"},{"key":"11_CR14","unstructured":"Magill, S., Nanevski, A., Clarke, E., Lee, P.: Inferring invariants in separation logic for imperative list-processing programs. In: Proceedings of SPACE Workshop (2006)"},{"issue":"10","key":"11_CR15","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u2018design by contract\u2019. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:\n                      10.1007\/978-3-540-78800-3_24"},{"issue":"11","key":"11_CR17","doi-asserted-by":"publisher","first-page":"1184","DOI":"10.1016\/j.jsc.2010.06.004","volume":"45","author":"Y Moy","year":"2010","unstructured":"Moy, Y., March\u00e9, C.: Modular inference of subprogram contracts for safety checking. J. Symbolic Comput. 45(11), 1184\u20131211 (2010)","journal-title":"J. Symbolic Comput."},{"issue":"6","key":"11_CR18","first-page":"397","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. JLAP 79(6), 397\u2013434 (2010)","journal-title":"JLAP"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1007\/11901433_39","volume-title":"Formal Methods and Software Engineering","author":"N Tillmann","year":"2006","unstructured":"Tillmann, N., Chen, F., Schulte, W.: Discovering likely method specifications. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 717\u2013736. Springer, Heidelberg (2006). doi:\n                      10.1007\/11901433_39"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Wei, Y., Furia, C.A., Kazmin, N., Meyer, B.: Inferring better contracts. In: Proceedings of the ICSE 2011, 191\u2013200. ACM (2011)","DOI":"10.1145\/1985793.1985820"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63139-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:51:39Z","timestamp":1558320699000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63139-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631387","9783319631394"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63139-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"25 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Edinburgh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.cliplab.org\/Conferences\/LOPSTR16\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}