{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:12:04Z","timestamp":1742980324968,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319681665"},{"type":"electronic","value":"9783319681672"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_20","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"289-306","source":"Crossref","is-referenced-by-count":3,"title":["Liquid Types for Array Invariant Synthesis"],"prefix":"10.1007","author":[{"given":"Manuel","family":"Montenegro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Susana","family":"Nieva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ricardo","family":"Pe\u00f1a","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clara","family":"Segura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2001), pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2006","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2006). doi:\n10.1007\/11609773_28"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2011, pp. 105\u2013118 (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"20_CR4","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-37036-6_8"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Launchbury, J., Mitchell, J.C. (eds.) 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002, pp. 191\u2013202. ACM (2002)","DOI":"10.1145\/503272.503291"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 338\u2013350 (2005)","DOI":"10.1145\/1040305.1040333"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL 2008, pp. 235\u2013246 (2008)","DOI":"10.1145\/1328438.1328468"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7\u201313, 2008, pp. 339\u2013348. ACM (2008)","DOI":"10.1145\/1375581.1375623"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Kawaguchi, M., Rondon, P.M., Jhala, R.: Type-based data structure verification. In: Hind, M., Diwan, A. (eds.) PLDI, pp. 304\u2013315. ACM (2009)","DOI":"10.1145\/1542476.1542510"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-27436-2_14","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M Montenegro","year":"2015","unstructured":"Montenegro, M., Pe\u00f1a, R., S\u00e1nchez-Hern\u00e1ndez, J.: A generic intermediate representation for verification condition generation. In: Falaschi, M. (ed.) LOPSTR 2015. LNCS, vol. 9527, pp. 227\u2013243. Springer, Cham (2015). doi:\n10.1007\/978-3-319-27436-2_14"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pp. 522\u2013538 (2016)","DOI":"10.1145\/2908080.2908093"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Gupta, R., Amarasinghe, S.P. (eds.) PLDI, pp. 159\u2013169. ACM (2008)","DOI":"10.1145\/1375581.1375602"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: Hind, M., Diwan, A. (eds.) PLDI, pp. 223\u2013234. ACM (2009)","DOI":"10.1145\/1542476.1542501"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), pp. 29\u201337. IEEE Computer Society Press (2001)","DOI":"10.1109\/LICS.2001.932480"},{"issue":"1","key":"20_CR16","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.: Verification decidability of presburger array programs. J. ACM 27(1), 191\u2013205 (1980)","journal-title":"J. ACM"},{"key":"20_CR17","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). doi:\n10.1007\/978-3-642-37036-6_13"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R.: LiquidHaskell: experience with refinement types in the real world. In: ACM SIGPLAN Symposium on Haskell 2014, pp. 39\u201351 (2014)","DOI":"10.1145\/2633357.2633366"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Jones, S.L.P.: Refinement types for Haskell. In: 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 269\u2013282 (2014)","DOI":"10.1145\/2628136.2628161"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,3]],"date-time":"2017-10-03T03:53:11Z","timestamp":1507002791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}