{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T10:10:11Z","timestamp":1746267011086,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":81,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662439470"},{"type":"electronic","value":"9783662439487"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43948-7_2","type":"book-chapter","created":{"date-parts":[[2014,6,11]],"date-time":"2014-06-11T16:10:36Z","timestamp":1402503036000},"page":"11-25","source":"Crossref","is-referenced-by-count":2,"title":["Verifying and Synthesizing Software with Recursive Functions"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11691617_9","volume-title":"Model Checking Software","author":"A. Armando","year":"2006","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 146\u2013162. Springer, Heidelberg (2006)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"issue":"8","key":"2_CR3","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.entcs.2006.11.037","volume":"174","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of recursive data types. Electronic Notes in Theoretical Computer Science\u00a0174(8), 23\u201337 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: POPL, pp. 221\u2013234 (2014)","DOI":"10.1145\/2535838.2535860"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"T.A. Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: SMT@IJCAR, pp. 3\u201311 (2012)","DOI":"10.29007\/1l7f"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 105\u2013125. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"2_CR10","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"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03237-0_1","volume-title":"Static Analysis","author":"R. Bodik","year":"2009","unstructured":"Bodik, R.: Algorithmic program synthesis with partial programs and decision procedures. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, p. 1. Springer, Heidelberg (2009)"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/321864.321875","volume":"22","author":"R.S. Boyer","year":"1975","unstructured":"Boyer, R.S., Moore, J.S.: Proving theorems about LISP functions. J. ACM\u00a022(1), 129\u2013144 (1975)","journal-title":"J. ACM"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-010-9211-0","volume":"49","author":"M. Codish","year":"2012","unstructured":"Codish, M., Giesl, J., Schneider-Kamp, P., Thiemann, R.: SAT solving for termination proofs with recursive path orders and dependency pairs. J. Autom. Reasoning\u00a049(1), 53\u201393 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR14","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn. MIT Press and McGraw-Hill (2001)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Darulov\u00e1, E., Kuncak, V.: Trustworthy numerical computation in scala. In: OOPSLA (2011)","DOI":"10.1145\/2048066.2048094"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-35632-2_27","volume-title":"Runtime Verification","author":"E. Darulova","year":"2013","unstructured":"Darulova, E., Kuncak, V.: Certifying solutions for numerical constraints. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol.\u00a07687, pp. 277\u2013291. Springer, Heidelberg (2013)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Sound compilation for reals. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (2014)","DOI":"10.1145\/2535838.2535874"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V., Majumdar, R., Saha, I.: Synthesis of fixed-point programs. In: Embedded Software (EMSOFT) (2013)","DOI":"10.1109\/EMSOFT.2013.6658600"},{"key":"2_CR19","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":"2_CR20","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":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-38574-2_12","volume-title":"Automated Deduction \u2013 CADE-24","author":"L.M. Moura de","year":"2013","unstructured":"de Moura, L.M., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 178\u2013192. Springer, Heidelberg (2013)"},{"issue":"3","key":"2_CR22","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 351\u2013368. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"2_CR24","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":"2_CR25","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416 (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Gvero, T., Kuncak, V., Kuraj, I., Piskac, R.: Complete completion using types and weights. In: PLDI (2013)","DOI":"10.1145\/2491956.2462192"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-22110-1_33","volume-title":"Computer Aided Verification","author":"T. Gvero","year":"2011","unstructured":"Gvero, T., Kuncak, V., Piskac, R.: Interactive synthesis of code snippets. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 418\u2013423. Springer, Heidelberg (2011)"},{"key":"2_CR28","unstructured":"Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: FMCAD (2010)"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL (2010)","DOI":"10.1145\/1706299.1706353"},{"key":"2_CR30","unstructured":"Hodges, W.: Model Theory. Encyclopedia of Mathematics and its Applications, vol.\u00a042. Cambridge University Press (1993)"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-33386-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"H. Hojjat","year":"2012","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 187\u2013202. Springer, Heidelberg (2012)"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-32759-9_21","volume-title":"FM 2012: Formal Methods","author":"H. Hojjat","year":"2012","unstructured":"Hojjat, H., Kone\u010dn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems (tool paper). In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 247\u2013251. Springer, Heidelberg (2012)"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-18275-4_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jacobs","year":"2011","unstructured":"Jacobs, S., Kuncak, V.: Towards complete reasoning about axiomatic specifications. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 278\u2013293. Springer, Heidelberg (2011)"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-38980-1","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, Springer, Heidelberg (2013)"},{"issue":"1","key":"2_CR36","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D. Jovanovic","year":"2013","unstructured":"Jovanovic, D., de Moura, L.M.: Cutting to the chase - solving linear integer arithmetic. J. Autom. Reasoning\u00a051(1), 79\u2013108 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: Pkind: A parallel k-induction based model checker. In: PDMC, pp. 55\u201362 (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuncak, V., Kuraj, I., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509555"},{"key":"2_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-54108-7_3","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Kneuss","year":"2014","unstructured":"Kneuss, E., Kuncak, V., Suter, P.: Effect analysis for programs with callbacks. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol.\u00a08164, pp. 48\u201367. Springer, Heidelberg (2014)"},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-16612-9_23","volume-title":"Runtime Verification","author":"E. Kneuss","year":"2010","unstructured":"Kneuss, E., Suter, P., Kuncak, V.: Runtime instrumentation for precise flow-sensitive type analysis. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 300\u2013314. Springer, Heidelberg (2010)"},{"key":"2_CR43","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":"2_CR44","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Blanc, R.: Interpolation for synthesis on unbounded domains. In: Formal Methods in Computer-Aided Design (FMCAD) (2013)","DOI":"10.1109\/FMCAD.2013.6679396"},{"key":"2_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-40787-1_1","volume-title":"Runtime Verification","author":"V. Kuncak","year":"2013","unstructured":"Kuncak, V., Kneuss, E., Suter, P.: Executing specifications using synthesis and constraint solving (invited talk). In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol.\u00a08174, pp. 1\u201320. Springer, Heidelberg (2013)"},{"key":"2_CR46","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":"2_CR47","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"},{"issue":"5-6","key":"2_CR48","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s10009-011-0217-7","volume":"15","author":"V. Kuncak","year":"2013","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. Software Tools for Technology Transfer (STTT)\u00a015(5-6), 455\u2013474 (2013)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"key":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-15205-4_5","volume-title":"Computer Science Logic","author":"V. Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures (invited paper). In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 34\u201348. Springer, Heidelberg (2010)"},{"key":"2_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-11319-2_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P., Wies, T.: Building a calculus of data structures (invited paper). In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 26\u201344. Springer, Heidelberg (2010)"},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"Lemay, A., Maneth, S., Niehren, J.: A learning algorithm for top-down xml transformations. In: PODS, pp. 285\u2013296 (2010)","DOI":"10.1145\/1807085.1807122"},{"key":"2_CR52","doi-asserted-by":"crossref","unstructured":"Madhavan, R., Kuncak, V.: Symbolic resource bound inference for functional programs. In: Computer Aided Verification (CAV) (2014)","DOI":"10.1007\/978-3-319-08867-9_51"},{"key":"2_CR53","unstructured":"Mal\u2019cev, A.I.: Axiomatizable classes of locally free algebras of various types. In: The Metamathematics of Algebraic Systems. North-Holland (1971); (Translation, original in Doklady, 1961)"},{"issue":"1","key":"2_CR54","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":"2_CR55","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":"2_CR56","doi-asserted-by":"crossref","unstructured":"Mayer, M., Kuncak, V.: Game programming by demonstration. In: SPLASH Onward! (2013)","DOI":"10.1145\/2509578.2509583"},{"key":"2_CR57","unstructured":"McMillan, K.L., Rybalchenko, A.: Solving constrained Horn clauses using interpolation. Technical Report MSR-TR-2013-6, Microsoft Research (January 2013)"},{"key":"2_CR58","doi-asserted-by":"crossref","unstructured":"Odersky, M.: Contracts for Scala. In: Int. Conf. Runtime Verification (2010)","DOI":"10.1007\/978-3-642-16612-9_5"},{"issue":"4","key":"2_CR59","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/2591013","volume":"57","author":"M. Odersky","year":"2014","unstructured":"Odersky, M., Rompf, T.: Unifying functional and object-oriented programming with Scala. Commun. ACM\u00a057(4), 76\u201386 (2014)","journal-title":"Commun. ACM"},{"key":"2_CR60","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: a comprehensive step-by-step guide. Artima Press (2008)"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511530104"},{"key":"2_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-87531-4_11","volume-title":"Computer Science Logic","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Fractional collections with cardinality bounds, and mixed integer linear arithmetic with stars. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 124\u2013138. Springer, Heidelberg (2008)"},{"key":"2_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-70545-1_25","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 268\u2013280. Springer, Heidelberg (2008)"},{"key":"2_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-14203-1_13","volume-title":"Automated Reasoning","author":"R. Piskac","year":"2010","unstructured":"Piskac, R., Kuncak, V.: Munch - automated reasoner for sets and multisets (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 149\u2013155. Springer, Heidelberg (2010)"},{"key":"2_CR65","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst.\u00a029(3) (2007)","DOI":"10.1145\/1232420.1232422"},{"key":"2_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54108-7_1","volume-title":"Verified Software: Theories, Tools, Experiments","author":"P. R\u00fcmmer","year":"2014","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Classifying and solving horn clauses for verification. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol.\u00a08164, pp. 1\u201321. Springer, Heidelberg (2014)"},{"key":"2_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P. R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 347\u2013363. Springer, Heidelberg (2013)"},{"key":"2_CR68","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 67\u201383. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_5"},{"key":"2_CR69","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, pp. 404\u2013415 (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"2_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-642-31365-3_39","volume-title":"Automated Reasoning","author":"A. Spielmann","year":"2012","unstructured":"Spielmann, A., Kuncak, V.: Synthesis for unbounded bitvector arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 499\u2013513. Springer, Heidelberg (2012)"},{"key":"2_CR71","unstructured":"Spielmann, A., N\u00f6tzli, A., Koch, C., Kuncak, V., Klonatos, Y.: Automatic synthesis of out-of-core algorithms. In: SIGMOD (2013)"},{"key":"2_CR72","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"},{"key":"2_CR73","unstructured":"Suter, P.: Programming with Specifications. PhD thesis, EPFL (December 2012)"},{"key":"2_CR74","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (2010)","DOI":"10.1145\/1706299.1706325"},{"key":"2_CR75","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"2_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-18275-4_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Suter","year":"2011","unstructured":"Suter, P., Steiger, R., Kuncak, V.: Sets with cardinality constraints in satisfiability modulo theories. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 403\u2013418. Springer, Heidelberg (2011)"},{"key":"2_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-22438-6_36","volume-title":"Automated Deduction \u2013 CADE-23","author":"T. Wies","year":"2011","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 476\u2013491. Springer, Heidelberg (2011)"},{"key":"2_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-27705-4_6","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T. Wies","year":"2012","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: Deciding functional lists with sublist sets. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 66\u201381. Springer, Heidelberg (2012)"},{"key":"2_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-642-04222-5_23","volume-title":"Frontiers of Combining Systems","author":"T. Wies","year":"2009","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 366\u2013382. Springer, Heidelberg (2009)"},{"key":"2_CR80","doi-asserted-by":"crossref","unstructured":"Yabandeh, M., Kne\u017eevi\u0107, N., Kosti\u0107, D., Kuncak, V.: Predicting and preventing inconsistencies in deployed distributed systems. ACM Transactions on Computer Systems\u00a028(1) (2010)","DOI":"10.1145\/1731060.1731062"},{"key":"2_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-642-11319-2_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Yessenov","year":"2010","unstructured":"Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 380\u2013395. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43948-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:31:08Z","timestamp":1746264668000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43948-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662439470","9783662439487"],"references-count":81,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43948-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}