{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:54:12Z","timestamp":1725749652551},"publisher-location":"Berlin, Heidelberg","reference-count":79,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642407864"},{"type":"electronic","value":"9783642407871"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40787-1_1","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T23:18:35Z","timestamp":1379546315000},"page":"1-20","source":"Crossref","is-referenced-by-count":6,"title":["Executing Specifications Using Synthesis and Constraint Solving"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Etienne","family":"Kneuss","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Ait-Kaci, H.: Warren\u2019s Abstract Machine: A Tutorial Reconstruction. MIT Press (1991)","DOI":"10.7551\/mitpress\/7160.001.0001"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Antoy, S.: Definitional trees. In: ALP, pp. 143\u2013157 (1992)","DOI":"10.1007\/BFb0013825"},{"issue":"4","key":"1_CR3","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1721654.1721675","volume":"53","author":"S. Antoy","year":"2010","unstructured":"Antoy, S., Hanus, M.: Functional logic programming. CACM\u00a053(4), 74\u201385 (2010)","journal-title":"CACM"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems II, pp. 1\u201320 (1995)","DOI":"10.1007\/3-540-60472-3_1"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Back, R.-J., von Wright, J.: In: Refinement Calculus, Springer (1998)","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058 (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Bierman, G.M., Gordon, A.D., Hritcu, C., Langworthy, D.E.: Semantic subtyping with an SMT solver. In: ICFP, pp. 105\u2013116 (2010)","DOI":"10.1145\/1932681.1863560"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system: Verification by translation to recursive functions. In: Scala Workshop (2013)","DOI":"10.1145\/2489837.2489838"},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/2220365.2220366","volume":"34","author":"E. Bodden","year":"2012","unstructured":"Bodden, E., Lam, P., Hendren, L.J.: Partially evaluating finite-state runtime monitors ahead of time. ACM Trans. Program. Lang. Syst.\u00a034(2), 7 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/978-3-540-77442-6_21","volume-title":"PADL","author":"B. Bra\u00dfel","year":"2008","unstructured":"Bra\u00dfel, B., Hanus, M., M\u00fcller, M.: High-level database programming in Curry. In: Hudak, P., Warren, D.S. (eds.) PADL 2008. LNCS, vol.\u00a04902, pp. 316\u2013332. Springer, Heidelberg (2008)"},{"issue":"12","key":"1_CR12","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0743-1066(89)90033-2","volume":"6","author":"M. Bruynooghe","year":"1989","unstructured":"Bruynooghe, M., Schreye, D.D., Krekels, B.: Compiling control. The Journal of Logic Programming\u00a06(12), 135\u2013162 (1989)","journal-title":"The Journal of Logic Programming"},{"key":"1_CR13","unstructured":"Butler, M., Grundy, J., Langbacka, T., Ruksenas, R., von Wright, J.: The refinement calculator: Proof support for program refinement. In: Formal Methods Pacific (1997)"},{"issue":"1","key":"1_CR14","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/227595.227597","volume":"43","author":"W. Chen","year":"1996","unstructured":"Chen, W., Warren, D.S.: Tabled evaluation with delaying for general logic programs. J. ACM\u00a043(1), 20\u201374 (1996)","journal-title":"J. ACM"},{"key":"1_CR15","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn. MIT Press and McGraw-Hill (2001)"},{"key":"1_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 de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer-Aided Design (November 2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Demsky, B., Rinard, M.C.: Automatic detection and repair of errors in data structures. In: OOPSLA, pp. 78\u201395 (2003)","DOI":"10.1145\/949343.949314"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Demsky, B., Rinard, M.C.: Data structure repair using goal-directed reasoning. In: ICSE, pp. 176\u2013185 (2005)","DOI":"10.1145\/1062455.1062499"},{"key":"1_CR20","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver (2006), http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Elkarablieh, B., Khurshid, S.: Juzi: a tool for repairing complex data structures. In: ICSE, pp. 855\u2013858 (2008)","DOI":"10.1145\/1368088.1368222"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Elkarablieh, B., Khurshid, S., Vu, D., McKinley, K.S.: Starc: static analysis for efficient repair of complex data. In: OOPSLA, pp. 387\u2013404 (2007)","DOI":"10.1145\/1297105.1297056"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"896","DOI":"10.1007\/978-3-642-39799-8_64","volume-title":"Computer Aided Verification","author":"C. Essen von","year":"2013","unstructured":"von Essen, C., Jobstmann, B.: Program repair without regret. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 896\u2013911. Springer, Heidelberg (2013)"},{"issue":"2","key":"1_CR24","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1023\/A:1008797606116","volume":"8","author":"P. Flener","year":"2001","unstructured":"Flener, P., Partridge, D.: Inductive programming. Autom. Softw. Eng.\u00a08(2), 131\u2013137 (2001)","journal-title":"Autom. Softw. Eng."},{"issue":"2-3","key":"1_CR25","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1012936614361","volume":"14","author":"J. Gallagher","year":"2001","unstructured":"Gallagher, J., Peralta, J.: Regular tree languages as an abstract domain in program specialisation. Higher-Order and Symbolic Computation\u00a014(2-3), 143\u2013172 (2001)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: International Conference on Software Engineering (ICSE) (2010)","DOI":"10.1145\/1806799.1806835"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62\u201373 (2011)","DOI":"10.1145\/1993316.1993506"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Hanus, M.: Type-oriented construction of web user interfaces. In: PPDP, pp. 27\u201338 (2006)","DOI":"10.1145\/1140335.1140341"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-92995-6_2","volume-title":"Practical Aspects of Declarative Languages","author":"M. Hanus","year":"2008","unstructured":"Hanus, M., Klu\u00df, C.: Declarative programming of user interfaces. In: Gill, A., Swift, T. (eds.) PADL 2009. LNCS, vol.\u00a05418, pp. 16\u201330. Springer, Heidelberg (2008)"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: IgorII - an analytical inductive functional programming system (tool demo). In: PEPM, pp. 29\u201332 (2010)","DOI":"10.1145\/1706356.1706364"},{"issue":"2","key":"1_CR31","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol.\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-35873-9_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jacobs","year":"2013","unstructured":"Jacobs, S., Kuncak, V., Suter, P.: Reductions for synthesis procedures. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 88\u2013107. Springer, Heidelberg (2013)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 258\u2013262. Springer, Heidelberg (2007)"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: PKIND: A parallel k-induction based model checker. In: 10th Int. Workshop Parallel and Distributed Methods in verifiCation, PDMC 2011 (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"1_CR36","first-page":"429","volume":"7","author":"E. Kitzelmann","year":"2006","unstructured":"Kitzelmann, E., Schmid, U.: Inductive synthesis of functional programs: An explanation based generalization approach. JMLR\u00a07, 429\u2013454 (2006)","journal-title":"JMLR"},{"key":"1_CR37","unstructured":"Kneuss, E., Kuncak, V., Kuraj, I., Suter, P.: On integrating deductive synthesis and verification systems. Technical Report EPFL-REPORT-186043, EPFL (2013)"},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-642-22438-6_30","volume-title":"Automated Deduction \u2013 CADE-23","author":"A.S. K\u00f6ksal","year":"2011","unstructured":"K\u00f6ksal, A.S., Kuncak, V., Suter, P.: Scala to the power of Z3: Integrating SMT and programming. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 400\u2013406. Springer, Heidelberg (2011)"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"K\u00f6ksal, A., Kuncak, V., Suter, P.: Constraints as control. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL (2012)","DOI":"10.1145\/2103656.2103675"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: ACM SIGPLAN Conf. Programming Language Design and Implementation, PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"key":"1_CR41","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. Software Tools for Technology Transfer (STTT), TBD (TBD) (2012)"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. Communications of the ACM (2012)","DOI":"10.1145\/2076450.2076472"},{"key":"1_CR43","unstructured":"Leino, K.R.M.: This is Boogie 2. Manuscript KRML 178, working draft (June 24, 2008)"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Malik, M.Z., Siddiqui, J.H., Khurshid, S.: Constraint-based program debugging using data structure repair. ICST, 190\u2013199 (2011)","DOI":"10.1109\/ICST.2011.65"},{"issue":"1","key":"1_CR45","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst.\u00a02(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"1_CR46","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/362566.362568","volume":"14","author":"Z. Manna","year":"1971","unstructured":"Manna, Z., Waldinger, R.J.: Toward automatic program synthesis. Commun. ACM\u00a014(3), 151\u2013165 (1971)","journal-title":"Commun. ACM"},{"key":"1_CR47","unstructured":"Michael Hanus, E.: Curry: An integrated functional logic language vers. 0.8.2 (2006), http:\/\/www.curry-language.org"},{"key":"1_CR48","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Rayside, D., Yessenov, K., Jackson, D.: Unifying execution of imperative and declarative code. In: ICSE, pp. 511\u2013520 (2011)","DOI":"10.1145\/1985793.1985863"},{"issue":"20","key":"1_CR49","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1016\/0743-1066(94)90035-3","volume":"19","author":"S. Muggleton","year":"1994","unstructured":"Muggleton, S., Raedt, L.D.: Inductive logic programming: Theory and methods. J. Log. Program.\u00a019(20), 629\u2013679 (1994)","journal-title":"J. Log. Program."},{"key":"1_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"1_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-16612-9_5","volume-title":"Runtime Verification","author":"M. Odersky","year":"2010","unstructured":"Odersky, M.: Contracts for Scala. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 51\u201357. Springer, Heidelberg (2010)"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511530104"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Pei, Y., Wei, Y., Furia, C.A., Nordio, M., Meyer, B.: Evidence-based automated program fixing. CoRR, abs\/1102.1059 (2011)","DOI":"10.1109\/ASE.2011.6100080"},{"key":"1_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2006)"},{"key":"1_CR55","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/75277.75293","volume-title":"POPL 1989: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179\u2013190. ACM, New York (1989)"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before. In: Int. Conf. Runtime Verification (2013)","DOI":"10.1007\/978-3-642-40787-1_15"},{"key":"1_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-642-14107-2_26","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"H. Samimi","year":"2010","unstructured":"Samimi, H., Aung, E.D., Millstein, T.: Falling back on executable specifications. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 552\u2013576. Springer, Heidelberg (2010)"},{"issue":"6","key":"1_CR58","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1017\/S0956796809990086","volume":"19","author":"T. Schrijvers","year":"2009","unstructured":"Schrijvers, T., Stuckey, P.J., Wadler, P.: Monadic constraint programming. J. Funct. Program.\u00a019(6), 663\u2013697 (2009)","journal-title":"J. Funct. Program."},{"key":"1_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-30473-6_10","volume-title":"Tests and Proofs","author":"V. Senni","year":"2012","unstructured":"Senni, V., Fioravanti, F.: Generation of test data structures using constraint logic programming. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol.\u00a07305, pp. 115\u2013131. Springer, Heidelberg (2012)"},{"key":"1_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-642-31424-7_44","volume-title":"Computer Aided Verification","author":"R. Singh","year":"2012","unstructured":"Singh, R., Gulwani, S.: Synthesizing number transformations from input-output examples. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 634\u2013651. Springer, Heidelberg (2012)"},{"key":"1_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-69149-5_20","volume-title":"Verified Software: Theories, Tools, Experiments","author":"D.R. Smith","year":"2008","unstructured":"Smith, D.R.: Generating programs plus proofs by refinement. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 182\u2013188. Springer, Heidelberg (2008)"},{"key":"1_CR62","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bod\u00edk, R., Saraswat, V.A., Seshia, S.A.: Sketching stencils. In: PLDI, pp. 167\u2013178 (2007)","DOI":"10.1145\/1273442.1250754"},{"key":"1_CR63","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bod\u00edk, R.: Sketching concurrent data structures. In: PLDI (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.: From program verification to program synthesis. In: POPL (2010)","DOI":"10.1145\/1706299.1706337"},{"issue":"1","key":"1_CR66","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1145\/321992.322002","volume":"24","author":"P.D. Summers","year":"1977","unstructured":"Summers, P.D.: A methodology for LISP program construction from examples. JACM\u00a024(1), 161\u2013175 (1977)","journal-title":"JACM"},{"key":"1_CR67","unstructured":"Suter, P.: Programming with Specifications. PhD thesis, EPFL (December 2012)"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: ACM POPL (2010)","DOI":"10.1145\/1706299.1706325"},{"key":"1_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-23702-7_23","volume-title":"Static Analysis","author":"P. Suter","year":"2011","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 298\u2013315. Springer, Heidelberg (2011)"},{"key":"1_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"1_CR71","doi-asserted-by":"crossref","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J., Mador-Haim, S., Martin, M., Alur, R.: Transit: Specifying protocols with concolic snippets. In: ACM Conference on Programming Language Design and Implementation (2013)","DOI":"10.1145\/2491956.2462174"},{"key":"1_CR72","unstructured":"Van Roy, P.: Logic programming in Oz with Mozart. In: ICLP (1999)"},{"key":"1_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-00768-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 139\u2013154. Springer, Heidelberg (2009)"},{"key":"1_CR74","doi-asserted-by":"crossref","unstructured":"Wei, Y., Furia, C.A., Kazmin, N., Meyer, B.: Inferring better contracts. In: ICSE (2011)","DOI":"10.1145\/1985793.1985820"},{"key":"1_CR75","doi-asserted-by":"crossref","unstructured":"Wei, Y., Pei, Y., Furia, C.A., Silva, L.S., Buchholz, S., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA 2010, pp. 61\u201372 (2010)","DOI":"10.1145\/1831708.1831716"},{"issue":"1","key":"1_CR76","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/357980.358010","volume":"26","author":"N. Wirth","year":"1983","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM\u00a026(1), 70\u201374 (1983) (reprint)","journal-title":"Commun. ACM"},{"key":"1_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/978-3-642-14107-2_27","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"R. Nokhbeh Zaeem","year":"2010","unstructured":"Nokhbeh Zaeem, R., Khurshid, S.: Contract-based data structure repair using alloy. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 577\u2013598. Springer, Heidelberg (2010)"},{"key":"1_CR78","unstructured":"Zaeem, R.N., Malik, M.Z., Khurshid, S.: Repair abstractions for more efficient data structure repair. In: Int. Conf. Runtime Verification (2013)"},{"key":"1_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-77395-5_17","volume-title":"Runtime Verification","author":"K. Zee","year":"2007","unstructured":"Zee, K., Kuncak, V., Taylor, M., Rinard, M.: Runtime checking for program verification. In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol.\u00a04839, pp. 202\u2013213. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40787-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,4]],"date-time":"2020-08-04T08:29:33Z","timestamp":1596529773000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40787-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642407864","9783642407871"],"references-count":79,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40787-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}