{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T22:00:47Z","timestamp":1726005647922},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030112448"},{"type":"electronic","value":"9783030112455"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-11245-5_13","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T13:45:18Z","timestamp":1547127918000},"page":"275-296","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Type-Directed Bounding of Collections in Reactive Programs"],"prefix":"10.1007","author":[{"given":"Tianhan","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavol","family":"\u010cern\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bor-Yuh Evan","family":"Chang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashutosh","family":"Trivedi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"key":"13_CR1","unstructured":"DARPA space-time analysis for cybersecurity program (STAC). http:\/\/www.darpa.mil\/program\/space-time-analysis-for-cybersecurity"},{"key":"13_CR2","unstructured":"Scala library for parsing and printing the SMT-LIB format. https:\/\/github.com\/regb\/scala-smtlib"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-71316-6_12","volume-title":"Programming Languages and Systems","author":"E Albert","year":"2007","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of Java bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157\u2013172. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_12"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., Gomez-Zamalloa, M.: Heap space analysis for Java bytecode. In: Proceedings of the 6th International Symposium on Memory Management, pp. 105\u2013116. ACM (2007)","DOI":"10.1145\/1296907.1296922"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., G\u00f3mez-Zamalloa Gil, M.: Live heap space analysis for languages with garbage collection. In: Proceedings of the 2009 International Symposium on Memory Management, pp. 129\u2013138. ACM (2009)","DOI":"10.1145\/1542431.1542450"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-642-18275-4_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Albert","year":"2011","unstructured":"Albert, E., Genaim, S., Masud, A.N.: More precise yet widely applicable cost analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 38\u201353. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_5"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-642-33125-1_27","volume-title":"Static Analysis","author":"DE Alonso-Blas","year":"2012","unstructured":"Alonso-Blas, D.E., Genaim, S.: On the limits of the classical approach to cost analysis. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 405\u2013421. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33125-1_27"},{"issue":"6","key":"13_CR8","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1145\/2813885.2737955","volume":"50","author":"Q Carbonneaux","year":"2015","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. ACM SIGPLAN Not. 50(6), 467\u2013478 (2015)","journal-title":"ACM SIGPLAN Not."},{"issue":"2\u20133","key":"13_CR9","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/A:1012996816178","volume":"14","author":"WN Chin","year":"2001","unstructured":"Chin, W.N., Khoo, S.C.: Calculating sized types. High.-Order Symb. Comput. 14(2\u20133), 261\u2013300 (2001)","journal-title":"High.-Order Symb. Comput."},{"key":"13_CR10","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/2666357.2597822","volume":"49","author":"D Coughlin","year":"2014","unstructured":"Coughlin, D., Chang, B.Y.E.: Fissile type analysis: modular checking of almost everywhere invariants. ACM SIGPLAN Not. 49, 73\u201385 (2014)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR11","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Dietl, W., Dietzel, S., Ernst, M.D., Mu\u015flu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 681\u2013690. ACM (2011)","DOI":"10.1145\/1985793.1985889"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-12736-1_15","volume-title":"Programming Languages and Systems","author":"A Flores-Montoya","year":"2014","unstructured":"Flores-Montoya, A., H\u00e4hnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275\u2013295. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12736-1_15"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-08587-6_13","volume-title":"Automated Reasoning","author":"J Giesl","year":"2014","unstructured":"Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184\u2013191. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_13"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1145\/1543135.1542518","volume":"44","author":"S Gulwani","year":"2009","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. ACM SIGPLAN Not. 44, 375\u2013385 (2009)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1145\/1594834.1480898","volume":"44","author":"S Gulwani","year":"2009","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. ACM SIGPLAN Not. 44, 127\u2013139 (2009)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/1809028.1806630","volume":"45","author":"S Gulwani","year":"2010","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. ACM SIGPLAN Not. 45, 292\u2013304 (2010)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1145\/1925844.1926427","volume":"46","author":"J Hoffmann","year":"2011","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM SIGPLAN Not. 46, 357\u2013370 (2011)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/3093333.3009842","volume":"52","author":"J Hoffmann","year":"2017","unstructured":"Hoffmann, J., Das, A., Weng, S.C.: Towards automatic resource bound analysis for OCaml. ACM SIGPLAN Not. 52, 359\u2013373 (2017)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1145\/2813885.2737966","volume":"50","author":"O Olivo","year":"2015","unstructured":"Olivo, O., Dillig, I., Lin, C.: Static detection of asymptotic performance bugs in collection traversals. ACM SIGPLAN Not. 50, 369\u2013378 (2015)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Papi, M.M., Ali, M., Correa Jr., T.L., Perkins, J.H., Ernst, M.D.: Practical pluggable types for Java. In: Proceedings of the 2008 International Symposium on Software Testing and Analysis, pp. 201\u2013212. ACM (2008)","DOI":"10.1145\/1390630.1390656"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1145\/1379022.1375602","volume":"43","author":"PM Rondon","year":"2008","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. ACM SIGPLAN Not. 43, 159\u2013169 (2008)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR23","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/1707801.1706316","volume":"45","author":"PM Rondon","year":"2010","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Low-level liquid types. ACM SIGPLAN Not. 45, 131\u2013144 (2010)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR24","doi-asserted-by":"crossref","first-page":"745","DOI":"10.1007\/978-3-319-08867-9_50","volume-title":"Computer Aided Verification","author":"Moritz Sinn","year":"2014","unstructured":"Sinn, M., Zuleger, F., Veith, H.: A simple and scalable approach to bound analysis and amortized complexity analysis. In: Computer Aided Verification-26th International Conference (CAV 14), pp. 743\u2013759 (2014)"},{"key":"13_CR25","unstructured":"Vasconcelos, P.B.: Space cost analysis using sized types. Ph.D. thesis, University of St Andrews (2008)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-27861-0_6","volume-title":"Implementation of Functional Languages","author":"PB Vasconcelos","year":"2004","unstructured":"Vasconcelos, P.B., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Trinder, P., Michaelson, G.J., Pe\u00f1a, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 86\u2013101. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27861-0_6"},{"key":"13_CR27","unstructured":"Lu, T., Cern\u00fd, P., Chang, B.-Y.E., Trivedi, A.: Type-directed bounding of collections in reactive programs. CoRR abs\/1810.10443 (2018)"},{"key":"13_CR28","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Xu, G., Rountev, A.: Precise memory leak detection for Java software using container profiling. In: Proceedings of the 30th International Conference on Software Engineering, pp. 151\u2013160. ACM (2008)","DOI":"10.1145\/1368088.1368110"},{"key":"13_CR30","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1145\/1809028.1806616","volume":"45","author":"G Xu","year":"2010","unstructured":"Xu, G., Rountev, A.: Detecting inefficiently-used containers to avoid bloat. ACM SIGPLAN Not. 45, 160\u2013173 (2010)","journal-title":"ACM SIGPLAN Not."},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-23702-7_22","volume-title":"Static Analysis","author":"F Zuleger","year":"2011","unstructured":"Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280\u2013297. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_22"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-11245-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T22:16:50Z","timestamp":1573683410000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cascais","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl19.sigplan.org\/track\/VMCAI-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}