{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,11]],"date-time":"2026-09-11T04:31:13Z","timestamp":1789101073296,"version":"build-2803163510"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319088662","type":"print"},{"value":"9783319088679","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_51","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T07:37:30Z","timestamp":1403941050000},"page":"762-778","source":"Crossref","is-referenced-by-count":8,"title":["Symbolic Resource Bound Inference for Functional Programs"],"prefix":"10.1007","author":[{"given":"Ravichandhran","family":"Madhavan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1","key":"51_CR1","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.tcs.2011.07.009","volume":"413","author":"E. Albert","year":"2012","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci.\u00a0413(1), 142\u2013159 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"51_CR2","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":"51_CR3","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":"51_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"51_CR5","doi-asserted-by":"crossref","unstructured":"Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system. In: Scala Workshop (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"51_CR6","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1145\/227234.227246","volume":"39","author":"G.E. Blelloch","year":"1996","unstructured":"Blelloch, G.E., Maggs, B.M.: Parallel algorithms. Communications of the ACM\u00a039, 85\u201397 (1996)","journal-title":"Communications of the ACM"},{"key":"51_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"51_CR8","doi-asserted-by":"crossref","unstructured":"Cook, B., Gupta, A., Magill, S., Rybalchenko, A., Simsa, J., Singh, S., Vafeiadis, V.: Finding heap-bounds for hardware synthesis. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351120"},{"key":"51_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"51_CR10","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.S.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"51_CR11","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"51_CR12","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kuncak, V., Losa, G.: Speculative linearizability. In: PLDI (2012)","DOI":"10.1145\/2254064.2254072"},{"key":"51_CR13","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI (2011)","DOI":"10.1145\/1993498.1993506"},{"key":"51_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: Precise and efficient static estimation of program computational complexity. In: POPL (2009)","DOI":"10.1145\/1480881.1480898"},{"key":"51_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"51_CR16","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":"51_CR17","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":"51_CR18","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509555"},{"issue":"7","key":"51_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"51_CR20","unstructured":"Madhavan, R., Kuncak, V.: Symbolic resource bound inference. Technical Report EPFL-REPORT-190578, EPFL (2014), \n                    \n                      http:\/\/infoscience.epfl.ch\/record\/190578"},{"key":"51_CR21","unstructured":"Makarios, T.J.M.: The independence of Tarski\u2019s Euclidean axiom. Archive of Formal Proofs, Formal proof development (October 2012), \n                    \n                      http:\/\/afp.sf.net\/entries\/Tarskis_Geometry.shtml\n                    \n                    \n                  ,"},{"key":"51_CR22","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: A comprehensive step-by-step guide. Artima Press (2008)"},{"key":"51_CR23","doi-asserted-by":"crossref","unstructured":"Oppen, D.C.: Elementary bounds for presburger arithmetic. In: Proceedings of the Fifth Annual ACM Symposium on Theory of Computing (1973)","DOI":"10.1145\/800125.804033"},{"key":"51_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"key":"51_CR25","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: POPL (2004)","DOI":"10.1145\/964001.964028"},{"key":"51_CR26","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":"51_CR27","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL (2010)","DOI":"10.1145\/1706299.1706325"},{"key":"51_CR28","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":"51_CR29","unstructured":"Yu, L.: A formal model of IEEE floating point arithmetic. Archive of Formal Proofs, Formal proof development (July 2013), \n                    \n                      http:\/\/afp.sf.net\/entries\/IEEE_Floating_Point.shtml"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_51","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T01:09:14Z","timestamp":1558919354000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}