{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:29:15Z","timestamp":1770272955154,"version":"3.49.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"12","license":[{"start":{"date-parts":[[2018,11,13]],"date-time":"2018-11-13T00:00:00Z","timestamp":1542067200000},"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":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s11432-017-9280-9","type":"journal-article","created":{"date-parts":[[2018,11,17]],"date-time":"2018-11-17T07:04:02Z","timestamp":1542438242000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal modelling of list based dynamic memory allocators"],"prefix":"10.1007","volume":"61","author":[{"given":"Bin","family":"Fang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wen","family":"Su","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Raymond","family":"Abrial","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Qiao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,11,13]]},"reference":[{"key":"9280_CR1","volume-title":"The Art of Computer Programming, Volume I: Fundamental Algorithms","author":"E K Donald","year":"1973","unstructured":"Donald E K. The Art of Computer Programming, Volume I: Fundamental Algorithms. 3rd ed. Upper Saddle River: Addison-Wesley, 1973"},{"key":"9280_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-60368-9_19","volume":"986","author":"R W Paul","year":"1995","unstructured":"Paul R W, Mark S J, Michael N, et al. Dynamic storage allocation: a survey and critical review. In: Proceedings of International Workshop on Memory Management, Kinross, 1995. 986: 1\u2013116","journal-title":"Proceedings of International Workshop on Memory Management"},{"key":"9280_CR3","volume-title":"The C Programming Language","author":"W K Brian","year":"1988","unstructured":"Brian W K, Dennis R. The C Programming Language. 2nd ed. Upper Saddle River: Prentice-Hall, 1988"},{"key":"9280_CR4","volume-title":"dlmalloc","author":"L Doug","year":"2012","unstructured":"Doug L. dlmalloc. 2012. ftp:\/\/gee.cs.oswego.edu\/pub\/misc\/malloc.c"},{"key":"9280_CR5","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11823230_13","volume":"4134","author":"C Cristiano","year":"2006","unstructured":"Cristiano C, Dino D, Peter W O, et al. Beyond reachability: shape abstraction in the presence of pointer arithmetic. In: Proceedings of Static Analysis Symposium, Seoul, 2006. 4134. 182\u2013203","journal-title":"Proceedings of Static Analysis Symposium"},{"key":"9280_CR6","first-page":"234","volume-title":"Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"C Adam","year":"2011","unstructured":"Adam C. Mostly-automated verification of low-level programs in computational separation logic. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, San Jose, 2011. 234\u2013245"},{"key":"9280_CR7","first-page":"207","volume-title":"Proceedings of ACM Symposium on Operating Systems Principles","author":"K Gerwin","year":"2009","unstructured":"Gerwin K, Kevin E, Gernot H, et al. seL4: formal verification of an OS kernel. In: Proceedings of ACM Symposium on Operating Systems Principles, Big Sky, 2009. 207\u2013220"},{"key":"9280_CR8","first-page":"400","volume":"4260","author":"M Nicolas","year":"2006","unstructured":"Nicolas M, Reynald A, Akinori Y. Formal verification of the heap manager of an operating system using separation logic. In: Proceedings of International Conference on Formal Engineering Methods, Macao, 2006. 4260. 400\u2013419","journal-title":"Proceedings of International Conference on Formal Engineering Methods"},{"key":"9280_CR9","first-page":"97","volume-title":"Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages","author":"T Harvey","year":"2007","unstructured":"Harvey T, Gerwin K, Michael N. Types, bytes, and separation logic. In: Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, Nice, 2007. 97\u2013108"},{"key":"9280_CR10","first-page":"1","volume-title":"Proceedings of European Association for Computer Science Logic","author":"WO Peter","year":"2001","unstructured":"Peter WO, John C R, Yang H. Local reasoning about programs that alter data structures. In: Proceedings of European Association for Computer Science Logic, Paris, 2001. 1\u201319"},{"key":"9280_CR11","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0167-6423(90)90025-9","volume":"14","author":"D R Smith","year":"1990","unstructured":"Smith D R, Lowry M R. Algorithm theories and design tactics. Sci Comput Programming, 1990, 14: 305\u2013321","journal-title":"Sci Comput Programming"},{"key":"9280_CR12","first-page":"35","volume":"1","author":"A Leslie","year":"2008","unstructured":"Leslie A. Memory allocation in C. Sci Embed Syst Programm, 2008, 1: 35\u201342","journal-title":"Sci Embed Syst Programm"},{"key":"9280_CR13","volume-title":"Inside memory management","author":"B Jonathan","year":"2004","unstructured":"Jonathan B. Inside memory management. 2004. http:\/\/www.ibm.com\/developerworks\/library\/l-memory\/sidefile.html"},{"key":"9280_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R. Modeling in Event-B: System and Software Engineering. Cambridge: Cambridge University Press, 2010"},{"key":"9280_CR15","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J R Abrial","year":"2010","unstructured":"Abrial J R, Butler M, Hallerstede S, et al. Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transfer, 2010, 12: 447\u2013466","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"9280_CR16","first-page":"104","volume-title":"Proceedings of ACM SIGPLAN International Symposium on Memory Management","author":"B Fang","year":"2017","unstructured":"Fang B, Sighireanu M. A refinement hierarchy for free list memory allocators. In: Proceedings of ACM SIGPLAN International Symposium on Memory Management, Barcelona, 2017. 104\u2013114"},{"key":"9280_CR17","volume-title":"A Refinement Hierarchy for Free List Memory Allocators","author":"B Fang","year":"2017","unstructured":"Fang B, Sighireanu M. A Refinement Hierarchy for Free List Memory Allocators. Research Report hal-01510166, IRIF. 2017"},{"key":"9280_CR18","volume-title":"Topsy -A Teachable Operating System","author":"F George","year":"2000","unstructured":"George F, Christian C, Eckart Z, et al. Topsy -A Teachable Operating System. Technical Report, Version 1.1, 20000322. 2000"},{"key":"9280_CR19","first-page":"79","volume-title":"Proceedings of Euromicro Conference on Real-Time Systems","author":"M Miguel","year":"2004","unstructured":"Miguel M, Ismael R, Alfons C, et al. TLSF: a new dynamic memory allocator for real-time systems. In: Proceedings of Euromicro Conference on Real-Time Systems, Catania, 2004. 79\u201386"},{"key":"9280_CR20","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-00867-2_9","volume-title":"Methods, Models and Tools for Fault Tolerance","author":"Q A Malik","year":"2009","unstructured":"Malik Q A, Lilius J, Laibinis L. Model-based testing using scenarios and Event-B refinements. In: Methods, Models and Tools for Fault Tolerance. Berlin: Springer, 2009. 177\u2013195"},{"key":"9280_CR21","first-page":"151","volume-title":"Proceedings of International Symposium on Logic-based Program Synthesis and Transformation","author":"B Fang","year":"2016","unstructured":"Fang B, Sighireanu M. Hierarchical shape abstraction for analysis of free-list memory allocators. In: Proceedings of International Symposium on Logic-based Program Synthesis and Transformation, Edinburgh, 2016. 151\u2013167"},{"key":"9280_CR22","first-page":"282","volume":"8931","author":"J C Liu","year":"2015","unstructured":"Liu J C, Xavier R. Abstraction of arrays based on non contiguous partitions. In: Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation, Paris, 2015. 8931. 282\u2013299","journal-title":"Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation"},{"key":"9280_CR23","first-page":"130","volume-title":"Proceedings of International Conference on Engineering of Complex Computer Systems","author":"W Su","year":"2015","unstructured":"Su W, Abrial J R, Pu G G, et al. Formal development of a real-time operating system memory manager. In: Proceedings of International Conference on Engineering of Complex Computer Systems, Gold Coast, 2015. 130\u2013139"},{"key":"9280_CR24","first-page":"441","volume-title":"Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages","author":"H Chris","year":"2009","unstructured":"Chris H, Erez P. Automated verification of practical garbage collectors. In: Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, Savannah, 2009. 441\u2013453"},{"key":"9280_CR25","first-page":"2010","volume":"28","author":"S C Qin","year":"2017","unstructured":"Qin S C, Xu ZW, Ming Z. Survey of research on program verification via separation logic. J Softw, 2017, 28: 2010\u20132025","journal-title":"J Softw"},{"key":"9280_CR26","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W N Chin","year":"2012","unstructured":"Chin W N, David C, Nguyen H H, et al. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci Comput Programming, 2012, 77: 1006\u20131036","journal-title":"Sci Comput Programming"},{"key":"9280_CR27","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.scico.2013.03.004","volume":"82","author":"S Qin","year":"2014","unstructured":"Qin S, He G, Luo C, et al. Automatically refining partial specifications for heap-manipulating programs. Sci Comput Programming, 2014, 82: 56\u201376","journal-title":"Sci Comput Programming"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-017-9280-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-017-9280-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-017-9280-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,18]],"date-time":"2020-01-18T14:10:07Z","timestamp":1579356607000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-017-9280-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,13]]},"references-count":27,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["9280"],"URL":"https:\/\/doi.org\/10.1007\/s11432-017-9280-9","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11,13]]},"assertion":[{"value":"26 June 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 September 2017","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 November 2017","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 November 2018","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"122103"}}