{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:19:36Z","timestamp":1781075976811,"version":"3.54.1"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030112448","type":"print"},{"value":"9783030112455","type":"electronic"}],"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_15","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T18:45:18Z","timestamp":1547145918000},"page":"318-341","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Decidable Logic for Tree Data-Structures with Measurements"],"prefix":"10.1007","author":[{"given":"Xiaokang","family":"Qiu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yanjun","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"key":"15_CR1","unstructured":"https:\/\/engineering.purdue.edu\/~xqiu\/dryad-dec"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 1\u20138 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-04081-8_13","volume-title":"CONCUR 2009 - Concurrency Theory","author":"A Bouajjani","year":"2009","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 178\u2013195. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04081-8_13"},{"issue":"9","key":"15_CR4","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"Wei-Ngan Chin","year":"2012","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program, 1006\u20131036 (2012)","journal-title":"Science of Computer Programming"},{"issue":"6","key":"15_CR5","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/1993316.1993526","volume":"46","author":"Adam Chlipala","year":"2011","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011, pp. 234\u2013245 (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 235\u2013249. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23217-6_16"},{"issue":"1","key":"15_CR7","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/0890-5401(90)90043-H","volume":"85","author":"B Courcelle","year":"1990","unstructured":"Courcelle, B.: The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Inf. Comput. 85(1), 12\u201375 (1990)","journal-title":"Inf. Comput."},{"issue":"2","key":"15_CR8","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1006\/jcss.2001.1816","volume":"64","author":"J Engelfriet","year":"2002","unstructured":"Engelfriet, J., Maneth, S.: Output string languages of compositions of deterministic macro tree transducers. J. Comput. Syst. Sci. 64(2), 350\u2013395 (2002)","journal-title":"J. Comput. Syst. Sci."},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Goldfarb, M., Jo, Y., Kulkarni, M.: General transformations for GPU execution of tree traversals. In: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis (Supercomputing), SC 2013 (2013)","DOI":"10.1145\/2503210.2503223"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"790","DOI":"10.1007\/978-3-642-39799-8_55","volume-title":"Computer Aided Verification","author":"C Haase","year":"2013","unstructured":"Haase, C., Ishtiaq, S., Ouaknine, J., Parkinson, M.J.: SeLoger: a tool for graph-based reasoning in separation logic. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 790\u2013795. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_55"},{"issue":"1","key":"15_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00236-009-0108-5","volume":"47","author":"P Habermehl","year":"2010","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: Automata-based verification of programs with tree updates. Acta Informatica 47(1), 1\u201331 (2010)","journal-title":"Acta Informatica"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Heinze, T.S., M\u00f8ller, A., Strocco, F.: Type safety analysis for Dart. In: Proceedings of 12th Dynamic Languages Symposium (DLS), October 2016","DOI":"10.1145\/2989225.2989226"},{"key":"15_CR13","unstructured":"Huang, K., Qiu, X., Tian, Q., Wang, Y.: Reconciling enumerative and symbolic search in syntax-guided synthesis (2018)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-38574-2_2","volume-title":"Automated Deduction \u2013 CADE-24","author":"R Iosif","year":"2013","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 21\u201338. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_2"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1007\/978-3-642-39799-8_53","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2013","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 756\u2013772. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_53"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Jo, Y., Kulkarni, M.: Enhancing locality for recursive traversals of recursive structures. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2011, pp. 463\u2013482. ACM, New York (2011)","DOI":"10.1145\/2048066.2048104"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Jo, Y., Kulkarni, M.: Automatically enhancing locality for tree traversals with traversal splicing. In: Proceedings of the 2012 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2012. ACM, New York (2012)","DOI":"10.1145\/2384616.2384643"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Kaki, G., Jagannathan, S.: A relational framework for higher-order shape analysis. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 311\u2013324. ACM, New York (2014)","DOI":"10.1145\/2628136.2628159"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 304\u2013315. ACM, New York (2009)","DOI":"10.1145\/1542476.1542510"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1993, pp. 196\u2013205. ACM, New York (1993)","DOI":"10.1145\/158511.158628"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Principles of Programming Languages (POPL 2008), p. 16. Association for Computing Machinery, Inc., January 2008","DOI":"10.1145\/1328438.1328461"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-41528-4_21","volume-title":"Computer Aided Verification","author":"QL Le","year":"2016","unstructured":"Le, Q.L., Sun, J., Chin, W.-N.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382\u2013404. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_21"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL 2011, pp. 611\u2013622. ACM (2011)","DOI":"10.1145\/1926385.1926455"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-23702-7_8","volume-title":"Static Analysis","author":"P Madhusudan","year":"2011","unstructured":"Madhusudan, P., Qiu, X.: Efficient decision procedures for heaps using STRAND. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 43\u201359. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_8"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: POPL 2012, pp. 123\u2013136. ACM (2012)","DOI":"10.1145\/2103656.2103673"},{"issue":"9\u201310","key":"15_CR27","doi-asserted-by":"publisher","first-page":"1187","DOI":"10.1016\/j.ic.2008.03.019","volume":"206","author":"A Maletti","year":"2008","unstructured":"Maletti, A.: Compositions of extended top-down tree transducers. Inf. Comput. 206(9\u201310), 1187\u20131196 (2008)","journal-title":"Inf. Comput."},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-72734-7_26","volume-title":"Logical Foundations of Computer Science","author":"Z Manna","year":"2007","unstructured":"Manna, Z., Sipma, H.B., Zhang, T.: Verifying balanced trees. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 363\u2013378. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72734-7_26"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476\u2013490. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_47"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Meyerovich, L.A., Bodik, R.: Fast and parallel webpage layout. In: Proceedings of the 19th International Conference on World Wide Web, WWW 2010. pp. 711\u2013720. ACM, New York (2010)","DOI":"10.1145\/1772690.1772763"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Meyerovich, L.A., Torok, M.E., Atkinson, E., Bodik, R.: Parallel schedule synthesis for attribute grammars. In: PPoPP 2013 (2013)","DOI":"10.1145\/2442516.2442535"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI 2001, pp. 221\u2013231. ACM, June 2001","DOI":"10.1145\/381694.378851"},{"key":"15_CR33","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":"15_CR34","doi-asserted-by":"crossref","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI 2011, pp. 556\u2013566 (2011)","DOI":"10.1145\/1993316.1993563"},{"key":"15_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: PLDI 2014, pp. 440\u2013451. ACM (2014)","DOI":"10.1145\/2666356.2594325"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Petrashko, D., Lhot\u00e1k, O., Odersky, M.: Miniphases: compilation using modular and efficient tree transformations. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pp. 201\u2013216. ACM, New York (2017)","DOI":"10.1145\/3062341.3062346"},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"Pham, T., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. CoRR abs\/1603.08769 (2016)","DOI":"10.1007\/s10817-016-9368-2"},{"key":"15_CR39","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.scico.2013.01.006","volume":"82","author":"P Philippaerts","year":"2014","unstructured":"Philippaerts, P., M\u00fchlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: industrial case studies. Sci. Comput. Program. 82, 77\u201397 (2014)","journal-title":"Sci. Comput. Program."},{"key":"15_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2013","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773\u2013789. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_54"},{"key":"15_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-319-08867-9_47","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711\u2013728. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_47"},{"key":"15_CR42","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI 2013, pp. 231\u2013242. ACM (2013)","DOI":"10.1145\/2491956.2462169"},{"key":"15_CR43","doi-asserted-by":"crossref","unstructured":"Rajbhandari, S., et al.: A domain-specific compiler for a parallel multiresolution adaptive numerical simulation environment. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2016, pp. 40:1\u201340:12. IEEE Press, Piscataway (2016)","DOI":"10.1109\/SC.2016.39"},{"key":"15_CR44","doi-asserted-by":"crossref","unstructured":"Rajbhandari, S., et al.: On fusing recursive traversals of Kd trees. In: Proceedings of the 25th International Conference on Compiler Construction, pp. 152\u2013162. ACM (2016)","DOI":"10.1145\/2892208.2892228"},{"key":"15_CR45","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE-CS (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"15_CR46","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 159\u2013169. ACM, New York (2008)","DOI":"10.1145\/1375581.1375602"},{"issue":"6","key":"15_CR47","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/3140587.3062362","volume":"52","author":"O Saarikivi","year":"2017","unstructured":"Saarikivi, O., Veanes, M., Mytkowicz, T., Musuvathi, M.: Fusing effectful comprehensions. SIGPLAN Not. 52(6), 17\u201332 (2017)","journal-title":"SIGPLAN Not."},{"issue":"OOPSLA","key":"15_CR48","doi-asserted-by":"publisher","first-page":"76:1","DOI":"10.1145\/3133900","volume":"1","author":"L Sakka","year":"2017","unstructured":"Sakka, L., Sundararajah, K., Kulkarni, M.: Treefuser: a framework for analyzing and fusing general recursive tree traversals. Proc. ACM Program. Lang. 1(OOPSLA), 76:1\u201376:30 (2017)","journal-title":"Proc. ACM Program. Lang."},{"issue":"1","key":"15_CR49","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1145\/1707801.1706325","volume":"45","author":"Philippe Suter","year":"2010","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL 2010, pp. 199\u2013210 (2010)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR50","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.) SAS 2011. LNCS, vol. 6887, pp. 298\u2013315. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_23"},{"key":"15_CR51","first-page":"569","volume":"70","author":"BA Trakhtenbrot","year":"1950","unstructured":"Trakhtenbrot, B.A.: The impossibility of an algorithm for the decision problem for finite domains. Doklady Akad. Nauk SSSR (N.S.) 70, 569\u2013572 (1950)","journal-title":"Doklady Akad. Nauk SSSR (N.S.)"},{"key":"15_CR52","doi-asserted-by":"crossref","unstructured":"Vazou, N., Bakst, A., Jhala, R.: Bounded refinement types. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp. 48\u201361. ACM, New York (2015)","DOI":"10.1145\/2784731.2784745"},{"key":"15_CR53","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). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_13"},{"key":"15_CR54","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R.: LiquidHaskell: experience with refinement types in the real world. In: Haskell (2014)","DOI":"10.1145\/2633357.2633366"},{"key":"15_CR55","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 269\u2013282. ACM, New York (2014)","DOI":"10.1145\/2628136.2628161"},{"issue":"2","key":"15_CR56","first-page":"53","volume":"2","author":"N Vazou","year":"2017","unstructured":"Vazou, N., et al.: Refinement reflection: complete verification with SMT. Proc. ACM Program. Lang. 2(2), 53 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/11690634_7","volume-title":"Foundations of Software Science and Computation Structures","author":"G Yorsh","year":"2006","unstructured":"Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FoSSaCS 2006. LNCS, vol. 3921, pp. 94\u2013110. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11690634_7"},{"issue":"10","key":"15_CR58","doi-asserted-by":"publisher","first-page":"1526","DOI":"10.1016\/j.ic.2006.03.004","volume":"204","author":"T Zhang","year":"2006","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. Inf. Comput. 204(10), 1526\u20131574 (2006)","journal-title":"Inf. Comput."}],"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_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,10]],"date-time":"2022-09-10T02:10:40Z","timestamp":1662775840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}