{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:27:41Z","timestamp":1759638461813,"version":"3.37.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2-4","license":[{"start":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T00:00:00Z","timestamp":1238112000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10817-009-9124-y","type":"journal-article","created":{"date-parts":[[2009,3,26]],"date-time":"2009-03-26T11:21:51Z","timestamp":1238066511000},"page":"229-264","source":"Crossref","is-referenced-by-count":18,"title":["Model Checking Dynamic Memory Allocation in Operating Systems"],"prefix":"10.1007","volume":"42","author":[{"given":"Mar\u00eda del Mar","family":"Gallardo","sequence":"first","affiliation":[]},{"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,3,27]]},"reference":[{"key":"9124_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. In: LICS \u201907: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pp. 151\u2013160. IEEE Computer Society, Washington, DC (2007)","DOI":"10.1109\/LICS.2007.19"},{"key":"9124_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: TACAS, pp. 467\u2013481, Barcelona, 29 March\u20132 April 2004","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"9124_CR3","doi-asserted-by":"crossref","unstructured":"Avots, D., Dalton, M., Benjamin, V., Livshits, Lam, M.S.: Improving software security with a C pointer analysis. In: ICSE \u201905: Proceedings of the 27th international conference on Software engineering, pp. 332\u2013341. ACM, New York (2005)","DOI":"10.1145\/1062455.1062520"},{"key":"9124_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI \u201901: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, pp. 203\u2013213. ACM, New York (2001)","DOI":"10.1145\/378795.378846"},{"issue":"3","key":"9124_CR5","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1023\/A:1020083231504","volume":"17","author":"B Bennett","year":"2002","unstructured":"Bennett, B., Cohn, A.G., Wolter, F., Zakharyaschev, M.: Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Appl. Intell. 17(3), 239\u2013251 (2002)","journal-title":"Appl. Intell."},{"issue":"5\u20136","key":"9124_CR6","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T., Jhala, R., Majumdar, R.: The software model checker BLAST. Int. J. Softw. Tools Technol. Transf. (STTT), 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"9124_CR7","doi-asserted-by":"crossref","unstructured":"Bogudlov, I., Lev-Ami, T., Reps, T.W., Sagiv, M.: Revamping TVLA: making parametric shape analysis competitive. In: CAV, pp. 221\u2013225, Berlin, 3\u20137 July 2007","DOI":"10.1007\/978-3-540-73368-3_25"},{"key":"9124_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: Proc. of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201905), Edinburgh, 4\u20138 April 2005","DOI":"10.1007\/978-3-540-31980-1_2"},{"key":"9124_CR9","first-page":"52","volume-title":"Static Analysis, vol. 2006","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. 2006, pp. 52\u201370. Springer, New York (2006)"},{"key":"9124_CR10","doi-asserted-by":"crossref","unstructured":"Brochenin, R., Demri, S., Lozes \u00c9.: Reasoning about sequences of memory states. In: LFCS, pp. 100\u2013114 (2007)","DOI":"10.1007\/978-3-540-72734-7_8"},{"key":"9124_CR11","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT, Cambridge (1999)"},{"key":"9124_CR12","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, S., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE \u201900: Proceedings of the 22nd international conference on Software engineering, pp. 439\u2013448. ACM, New York (2000)","DOI":"10.1145\/337180.337234"},{"key":"9124_CR13","doi-asserted-by":"crossref","unstructured":"de\u00a0la C\u00e1mara, P., Gallardo, M.M., Merino, P., San\u00e1n, D.: Model checking software with well-defined APIs: the socket case. In: FMICS \u201905: Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, pp. 17\u201326. ACM, New York (2005)","DOI":"10.1145\/1081180.1081184"},{"key":"9124_CR14","doi-asserted-by":"crossref","unstructured":"de\u00a0la C\u00e1mara, P., Gallardo, M.M., Merino, P.: Model extraction for ARINC 653 based avionics software. In: SPIN, pp. 243\u2013262, Berlin, 1\u20133 July 2007","DOI":"10.1007\/978-3-540-73370-6_16"},{"key":"9124_CR15","doi-asserted-by":"crossref","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. 261\u2013276. Springer, London (1999)","DOI":"10.1007\/3-540-48234-2_20"},{"key":"9124_CR16","first-page":"287","volume-title":"In TACAS","author":"D Distefano","year":"2006","unstructured":"Distefano, D., Ohearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: In TACAS, pp. 287\u2013302. Springer, New York (2006)"},{"key":"9124_CR17","first-page":"41","volume-title":"Banff Higher Order Workshop","author":"E Allen Emerson","year":"1995","unstructured":"Allen Emerson, E.: Automated temporal reasoning about reactive systems. In: Banff Higher Order Workshop, pp. 41\u2013101. Springer, New York (1995)"},{"key":"9124_CR18","doi-asserted-by":"crossref","unstructured":"Fradet, P., Le M\u00e9tayer, D.: Shape types. In: POPL \u201997: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 27\u201339. ACM, New York (1997)","DOI":"10.1145\/263699.263706"},{"key":"9124_CR19","doi-asserted-by":"crossref","unstructured":"Gallardo, M.M., Merino, P., Joubert, C., Sanan, D.: On-the-fly model checking for C programs with extended CADP in FMICS-jETI. In: ICECCS \u201907: Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007), pp. 321\u2013329. IEEE Computer Society, Washington, DC (2007)","DOI":"10.1109\/ICECCS.2007.32"},{"key":"9124_CR20","unstructured":"Gallardo, M.M., Merino, P., Sanan, D.: Model checking C programs with dynamic memory allocation. In: to appear in the Proc. of the 32nd Annual IEEE International Computer Software and Applications Conference COMPSAC2008, Turku, 28 July\u20131 August 2008"},{"issue":"2","key":"9124_CR21","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: The Verisoft approach. Form. Methods Syst. Des. 26(2), 77\u2013101 (2005)","journal-title":"Form. Methods Syst. Des."},{"issue":"4","key":"9124_CR22","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. STTT, 2(4), 366\u2013381 (2000)","journal-title":"STTT"},{"key":"9124_CR23","doi-asserted-by":"crossref","unstructured":"Hendren, L.J., Hummell, J., Nicolau, A.: Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs. In: PLDI \u201992: Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, pp. 249\u2013260. ACM, New York (1992)","DOI":"10.1145\/143095.143138"},{"key":"9124_CR24","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295","DOI":"10.1109\/32.588521"},{"key":"9124_CR25","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"issue":"2","key":"9124_CR26","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1002\/stvr.228","volume":"11","author":"GJ Holzmann","year":"2001","unstructured":"Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verif. Reliab. 11(2), 65\u201379 (2001)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"9124_CR27","doi-asserted-by":"crossref","unstructured":"Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: SPIN, pp. 299\u2013305, Vienna, 30 March\u20131 April 2006","DOI":"10.1007\/11691617_19"},{"key":"9124_CR28","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: POPL, pp. 196\u2013205, Charleston, January 1993","DOI":"10.1145\/158511.158628"},{"key":"9124_CR29","doi-asserted-by":"crossref","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: SPIN \u201901: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, pp. 80\u2013102. Springer, New York (2001)","DOI":"10.1007\/3-540-45139-0_6"},{"key":"9124_CR30","doi-asserted-by":"crossref","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Proc. of VMCAI05. LNCS, vol. 3385, pp. 181\u2013198. Springer, New York (2005)","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"9124_CR31","unstructured":"M\u00f8ller, A.: Verifying programs that manipulate pointers: (invited talk). In: Proceedings of INFINITY 2003, the 5th International Workshop on Verification of Infinite-State Systems. Elect. Notes Theor. Comp. Sci. 98, 3\u20134 (2004)"},{"key":"9124_CR32","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI \u201901: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pp. 221\u2013231. ACM, New York (2001)","DOI":"10.1145\/378795.378851"},{"issue":"SI","key":"9124_CR33","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. SIGOPS Oper. Syst. Rev. 36(SI), 75\u201388 (2002)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"9124_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)"},{"key":"9124_CR35","unstructured":"Partow, A.: General purpose hash function algorithms. http:\/\/www.partow.net\/programming\/hashfunctions\/"},{"key":"9124_CR36","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374, Copenhagen, 22\u201325 July 2002","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9124_CR37","doi-asserted-by":"crossref","unstructured":"Robby, S., Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: ESEC\/FSE-11: Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 267\u2013276. ACM, New York (2003)","DOI":"10.1145\/940071.940107"},{"key":"9124_CR38","doi-asserted-by":"crossref","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. 105\u2013118. ACM, New York (1999)","DOI":"10.1145\/292540.292552"},{"key":"9124_CR39","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332\u2013344, Cambridge, 16\u201318 June 1986"},{"key":"9124_CR40","doi-asserted-by":"crossref","unstructured":"Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: ESOP2003: European Symp. on Programming. LNCS, vol. 2618, pp. 204\u2013222. Springer, New York (2003)","DOI":"10.1007\/3-540-36575-3_15"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9124-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9124-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9124-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T17:56:05Z","timestamp":1739037365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9124-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,27]]},"references-count":40,"journal-issue":{"issue":"2-4","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["9124"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9124-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2009,3,27]]}}}