{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:41Z","timestamp":1763468261750,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175232"},{"type":"electronic","value":"9783319175249"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_2","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"12-15","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Developing Verified Software Using Leon"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"2_CR1","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_CR2","unstructured":"Darulova, E.: Programming with Numerical Uncertainties. PhD thesis, EPFL (2014)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Darulova, E., Kuncak, V.: Sound compilation of reals. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (2014)","DOI":"10.1145\/2535838.2535874"},{"key":"2_CR4","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 de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR5","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_CR6","first-page":"29","volume":"146","author":"R Hindley","year":"1969","unstructured":"Hindley, R.: The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146, 29\u201360 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"2_CR7","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. 7737, pp. 88\u2013107. Springer, Heidelberg (2013)"},{"key":"2_CR8","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Koukoutos, M., Kuncak, V.: On deductive program repair in Leon. Technical Report EPFL-REPORT-205054, EPFL, February 2014","DOI":"10.1007\/978-3-319-21668-3_13"},{"key":"2_CR10","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_CR11","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_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-319-11164-3_22","volume-title":"Runtime Verification","author":"E Koukoutos","year":"2014","unstructured":"Koukoutos, E., Kuncak, V.: Checking data structure properties orders of magnitude faster. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 263\u2013268. Springer, Heidelberg (2014)"},{"key":"2_CR13","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. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 1\u201320. Springer, Heidelberg (2013)"},{"key":"2_CR14","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_CR15","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\u20136","key":"2_CR16","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) 15(5\u20136), 455\u2013474 (2013)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Kuraj, I., Kuncak, V.: SciFe: scala framework for effcient enumeration of data structures with invariants. In: Scala Workshop (2014)","DOI":"10.1145\/2637647.2637655"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/978-3-319-08867-9_51","volume-title":"Computer Aided Verification","author":"R Madhavan","year":"2014","unstructured":"Madhavan, R., Kuncak, V.: Symbolic resource bound inference for functional programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 762\u2013778. Springer, Heidelberg (2014)"},{"issue":"3","key":"2_CR19","first-page":"348","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. JCSS 17(3), 348\u2013375 (1978)","journal-title":"JCSS"},{"key":"2_CR20","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., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 51\u201357. Springer, Heidelberg (2010)"},{"key":"2_CR21","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in scala: a comprehensive step-by-step guide. Artima Press (2008)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., de Moura, L.M.: Finding conflicting instances of quantified formulas in SMT. In: FMCAD, pp. 195\u2013202. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"2_CR24","unstructured":"Suter, P.: Programming with Specifications. PhD thesis, EPFL, December 2012"},{"key":"2_CR25","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_CR26","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.) Static Analysis. LNCS, vol. 6887, pp. 298\u2013315. Springer, Heidelberg (2011)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-37036-6_13","volume-title":"Programming Languages and Systems","author":"N Vazou","year":"2013","unstructured":"Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209\u2013228. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T07:51:22Z","timestamp":1676015482000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}