{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,27]],"date-time":"2023-06-27T05:40:03Z","timestamp":1687844403760},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,10,16]],"date-time":"2012-10-16T00:00:00Z","timestamp":1350345600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2013,12]]},"DOI":"10.1007\/s10515-012-0113-8","type":"journal-article","created":{"date-parts":[[2012,10,17]],"date-time":"2012-10-17T22:10:38Z","timestamp":1350511838000},"page":"569-612","source":"Crossref","is-referenced-by-count":1,"title":["Verification of complex dynamic data tree with mu-calculus"],"prefix":"10.1007","volume":"20","author":[{"given":"Mar\u00eda","family":"del Mar\u00a0Gallardo","sequence":"first","affiliation":[]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,10,16]]},"reference":[{"issue":"1","key":"113_CR1","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/s10009-008-0090-1","volume":"11","author":"S. Anand","year":"2009","unstructured":"Anand, S., Pasareanu, C.S., Visser, W.: Symbolic execution with abstraction. Int. J. Softw. Tools Technol. Transf. 11(1), 53\u201367 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"113_CR2","first-page":"332","volume-title":"ICSE \u201905: Proceedings of the 27th International Conference on Software Engineering","author":"D. Avots","year":"2005","unstructured":"Avots, D., Dalton, M., Livshits, V.B., Lam, M.S.: Improving software security with a C pointer analysis. In: ICSE \u201905: Proceedings of the 27th International Conference on Software Engineering, pp.\u00a0332\u2013341. ACM, New York (2005)"},{"key":"113_CR3","first-page":"115","volume-title":"International Symposium on Formal Methods for Components and Objects","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: International Symposium on Formal Methods for Components and Objects, pp.\u00a0115\u2013137. Springer, Berlin (2005)"},{"key":"113_CR4","first-page":"178","volume-title":"CAV","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: CAV, pp.\u00a0178\u2013192. Springer, Berlin (2007)"},{"key":"113_CR5","first-page":"221","volume-title":"CAV","author":"I. Bogudlov","year":"2007","unstructured":"Bogudlov, I., Lev-Ami, T., Reps, T.W., Sagiv, M.: Revamping TVLA: making parametric shape analysis competitive. In: CAV, pp.\u00a0221\u2013225 (2007)"},{"key":"113_CR6","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/11823230_5","volume-title":"Static Analysis","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Static Analysis, vol.\u00a02006, pp.\u00a052\u201370. Springer, Berlin (2006)"},{"key":"113_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-540-72734-7_8","volume-title":"Logical Foundations of Computer Science","author":"R. Brochenin","year":"2007","unstructured":"Brochenin, R., Demri, S., Lozes, E.: Reasoning about sequences of memory states. In: Artemov, S., Nerode, A. (eds.) Logical Foundations of Computer Science. Lecture Notes in Computer Science, vol.\u00a04514, pp.\u00a0100\u2013114. Springer, Berlin (2007)"},{"key":"113_CR8","first-page":"289","volume-title":"Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL\u00a0\u201909","author":"C. Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL\u00a0\u201909, pp.\u00a0289\u2013300. ACM, New York (2009)"},{"key":"113_CR9","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"113_CR10","first-page":"48","volume-title":"Formal Methods in System Design","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In: Formal Methods in System Design, pp.\u00a048\u201358. Springer, Berlin (1993)"},{"key":"113_CR11","first-page":"439","volume-title":"ICSE\u00a0\u201900: Proceedings of the 22nd International Conference on Software Engineering","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE\u00a0\u201900: Proceedings of the 22nd International Conference on Software Engineering, pp.\u00a0439\u2013448. ACM, New York (2000)"},{"key":"113_CR12","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/3-540-48234-2_20","volume-title":"Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking","author":"C. Demartini","year":"1999","unstructured":"Demartini, C., Iosif, R., Sisto, R.: dSPIN: a dynamic extension of SPIN. In: Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, pp.\u00a0261\u2013276. Springer, London (1999)"},{"key":"113_CR13","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1449764.1449782","volume-title":"OOPSLA","author":"D. Distefano","year":"2008","unstructured":"Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA, pp.\u00a0213\u2013226 (2008)"},{"key":"113_CR14","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","first-page":"185","volume-title":"Descriptive Complexity and Finite Models","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A.: Model checking and the mu-calculus. In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a031, pp.\u00a0185\u2013214. Am. Math. Soc., Providence (1996)"},{"key":"113_CR15","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1109\/SEFM.2010.34","volume-title":"Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM\u00a0\u201910","author":"M.M. Gallardo","year":"2010","unstructured":"Gallardo, M.M., San\u00e1n, D.: Verification of dynamic data tree with mu-calculus extended with separation. In: Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM\u00a0\u201910, pp.\u00a0211\u2013221. IEEE Comput. Soc., Washington (2010)"},{"key":"113_CR16","first-page":"395","volume-title":"SAS","author":"M.M. Gallardo","year":"2002","unstructured":"Gallardo, M.M., Merino, P., Pimentel, E.: Refinement of LTL formulas for abstract model checking. In: SAS, pp.\u00a0395\u2013410 (2002)"},{"key":"113_CR17","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/s10009-003-0122-9","volume":"5","author":"M.M. Gallardo","year":"2004","unstructured":"Gallardo, M.M., Martinez, J., Merino, P., Pimentel, E.: aSPIN: a tool for abstract model checking. Int. J. Softw. Tools Technol. Transf. 5, 165\u2013184 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"113_CR18","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10817-009-9124-y","volume":"42","author":"M.M. Gallardo","year":"2009","unstructured":"Gallardo, M.M., Merino, P., San\u00e1n, D.: Model checking dynamic memory allocation in operating systems. J. Autom. Reason. 42(2), 229\u2013264 (2009)","journal-title":"J. Autom. Reason."},{"key":"113_CR19","first-page":"158","volume-title":"Proc. of CAV\u201907","author":"H. Garavel","year":"2007","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: a\u00a0toolbox for the construction and analysis of distributed processes. In: Proc. of CAV\u201907, pp.\u00a0158\u2013163 (2007)"},{"issue":"4","key":"113_CR20","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"113_CR21","first-page":"301","volume-title":"Formal Methods in System Design","author":"G. Holzmann","year":"1995","unstructured":"Holzmann, G.: An analysis of bitstate hashing. In: Formal Methods in System Design, pp.\u00a0301\u2013314. Chapman & Hall, London (1995)"},{"key":"113_CR22","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"113_CR23","first-page":"76","volume-title":"SPIN","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: SPIN, pp.\u00a076\u201391 (2004)"},{"key":"113_CR24","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"ESOP\u00a0\u201901: Proceedings of the 10th European Symposium on Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: ESOP\u00a0\u201901: Proceedings of the 10th European Symposium on Programming Languages and Systems, pp.\u00a0155\u2013169. Springer, London (2001)"},{"key":"113_CR25","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0553\u2013568. Springer, Berlin (2003)"},{"key":"113_CR26","first-page":"196","volume-title":"POPL","author":"N. Klarlund","year":"1993","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: POPL, pp.\u00a0196\u2013205 (1993)"},{"key":"113_CR27","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/3-540-45139-0_6","volume-title":"Proceedings of the 8th International SPIN Workshop on Model Checking of Software, SPIN\u00a0\u201901","author":"F. Lerda","year":"2001","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, SPIN\u00a0\u201901, pp.\u00a080\u2013102. Springer, New York (2001)"},{"key":"113_CR28","series-title":"LNCS","first-page":"181","volume-title":"Proc. of VMCAI05","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Proc. of VMCAI05. LNCS, vol.\u00a03385, pp.\u00a0181\u2013198. Springer, Berlin (2005)"},{"key":"113_CR29","first-page":"221","volume-title":"Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp.\u00a0221\u2013231 (2001)"},{"issue":"SI","key":"113_CR30","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/844128.844136","volume":"36","author":"M. Musuvathi","year":"2002","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: a pragmatic approach to model checking real code. Oper. Syst. Rev. 36(SI), 75\u201388 (2002)","journal-title":"Oper. Syst. Rev."},{"key":"113_CR31","first-page":"55","volume-title":"LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp.\u00a055\u201374 (2002)"},{"key":"113_CR32","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/292540.292552","volume-title":"POPL \u201999: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"M. Sagiv","year":"1999","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL \u201999: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.\u00a0105\u2013118. ACM, New York (1999)"},{"key":"113_CR33","first-page":"149","volume-title":"Proceedings of the VIII Banff Higher Order Workshop Conference on Logics for Concurrency: Structure Versus Automata","author":"C. Stirling","year":"1996","unstructured":"Stirling, C.: Modal and temporal logics for processes. In: Proceedings of the VIII Banff Higher Order Workshop Conference on Logics for Concurrency: Structure Versus Automata, pp.\u00a0149\u2013237. Springer, New York (1996)"},{"key":"113_CR34","first-page":"3","volume-title":"ASE","author":"W. Visser","year":"2000","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In: ASE, pp.\u00a03\u201312 (2000)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-012-0113-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-012-0113-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-012-0113-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T08:05:02Z","timestamp":1687766702000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-012-0113-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,16]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["113"],"URL":"https:\/\/doi.org\/10.1007\/s10515-012-0113-8","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,16]]}}}