{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:39:15Z","timestamp":1770273555131,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030355395","type":"print"},{"value":"9783030355401","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-35540-1_8","type":"book-chapter","created":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:01:29Z","timestamp":1574035289000},"page":"122-138","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Verified Specification of TLSF Memory Management Allocator Using State Monads"],"prefix":"10.1007","author":[{"given":"Yu","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongwang","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Sanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Qiao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jinkun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,18]]},"reference":[{"key":"8_CR1","unstructured":"TLSF: Memory allocator real time embedded systems. \nhttp:\/\/www.gii.upv.es\/tlsf\/"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Masmano, M., Ripoll, I., Crespo, A., Real, J.: TLSF: a new dynamic memory allocator for real-time systems. In: Proceedings of the 16th Euromicro Conference on Real-Time Systems, ECRTS 2004, Catania, Italy, 2004, pp. 79\u201388.\nhttps:\/\/doi.org\/10.1109\/EMRTS.2004.1311009","DOI":"10.1109\/EMRTS.2004.1311009"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"995","DOI":"10.1002\/spe.858","volume":"38","author":"M Masmano","year":"2008","unstructured":"Masmano, M., Ripoll, I., Real, J., Crespo, A., Wellings, A.J.: Implementation of a constant time dynamic storage allocator. Softw. Pract. Exp. 38, 995\u20131026 (2008). \nhttps:\/\/doi.org\/10.1002\/spe.858","journal-title":"Softw. Pract. Exp."},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167\u2013182. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_16"},{"key":"8_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Saraswat, V.A., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pp. 161\u2013172. ACM (2007)","DOI":"10.1145\/1229428.1229469"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36575-3_25","volume-title":"Programming Languages and Systems","author":"D Yu","year":"2003","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building Certified libraries for PCC: dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 363\u2013379. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-36575-3_25"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1\u201331 (2008)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-009-9122-0","volume":"42","author":"H Tews","year":"2009","unstructured":"Tews, H., V\u00f6lp, M., Weber, T.: Formal memory models for the verification of low-level operating-system code. J. Autom. Reason. 42(2), 189\u2013227 (2009)","journal-title":"J. Autom. Reason."},{"issue":"2-4","key":"8_CR10","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-009-9124-y","volume":"42","author":"Mar\u00eda del Mar Gallardo","year":"2009","unstructured":"Gallardo, M.d.M., Merino, P., San\u00e1n, D.: Model checking dynamic memory allocation in operating systems. J. Autom. Reason. 42(2), 229\u2013264 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"8_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2487241.2487248","volume":"60","author":"Jaroslav \u0160ev\u010d\u00edk","year":"2013","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM (JACM) 60(3), 22:1\u201322:50 (2013)","journal-title":"Journal of the ACM"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-319-21668-3_24","volume-title":"Computer Aided Verification","author":"W Mansky","year":"2015","unstructured":"Mansky, W., Garbuzov, D., Zdancewic, S.: An axiomatic specification for sequential memory models. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 413\u2013428. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21668-3_24"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-35308-6_13","volume-title":"Certified Programs and Proofs","author":"A Vaynberg","year":"2012","unstructured":"Vaynberg, A., Shao, Z.: Compositional verification of a baby virtual memory manager. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 143\u2013159. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-35308-6_13"},{"key":"8_CR14","unstructured":"Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Savannah, GA, pp. 653\u2013669. USENIX Association (2016)"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: 22nd ACM SIGOPS Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220. ACM Press (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"8_CR16","unstructured":"Klein, G., Tuch, H.: Towards verified virtual memory in L4. In: TPHOLs Emerging Trends, Park City, Utah, USA, 16 pages, September 2004"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-540-78800-3_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Alkassar","year":"2008","unstructured":"Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 109\u2013123. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_9"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-19458-5_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"A Blanchard","year":"2015","unstructured":"Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with frama-C. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 15\u201330. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19458-5_2"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-662-49665-7_13","volume-title":"Fundamental Approaches to Software Engineering","author":"P Bolignano","year":"2016","unstructured":"Bolignano, P., Jensen, T., Siles, V.: Modeling and abstraction of memory management in a hypervisor. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 214\u2013230. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49665-7_13"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Su, W., Abrial, J., Pu, G., Fang, B.: Formal development of a real-time operating system memory manager. In: 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS), Gold Coast, QLD, pp. 130\u2013139 (2015). \nhttps:\/\/doi.org\/10.1109\/ICECCS.2015.24","DOI":"10.1109\/ICECCS.2015.24"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-63139-4_9","volume-title":"Logic-Based Program Synthesis and Transformation","author":"B Fang","year":"2017","unstructured":"Fang, B., Sighireanu, M.: Hierarchical shape abstraction for analysis of free list memory allocators. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 151\u2013167. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63139-4_9"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Fang, B., Sighireanu, M.: A refinement hierarchy for free list memory allocators. In: Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management, pp. 104\u2013114. ACM (2017)","DOI":"10.1145\/3156685.3092275"},{"issue":"12","key":"8_CR23","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s11432-017-9280-9","volume":"61","author":"B Fang","year":"2018","unstructured":"Fang, B., Sighireanu, M., Pu, G., Su, W., Abrial, J.R., Yang, M., Qiao, L.: Formal modelling of list based dynamic memory allocators. Sci. China Inf. Sci. 61(12), 103\u2013122 (2018)","journal-title":"Sci. China Inf. Sci."},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/11901433_22","volume-title":"Formal Methods and Software Engineering","author":"N Marti","year":"2006","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Formal verification of the heap manager of an operating system using separation logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 400\u2013419. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11901433_22"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-35540-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:23:03Z","timestamp":1574036583000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-35540-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030355395","9783030355401"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-35540-1_8","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":"18 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shanghai","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"27 November 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2019a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www4.comp.polyu.edu.hk\/~csguannan\/setta19\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}