{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,19]],"date-time":"2025-10-19T15:48:11Z","timestamp":1760888891277},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T00:00:00Z","timestamp":1395100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10009-014-0307-4","type":"journal-article","created":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T01:14:43Z","timestamp":1395105283000},"page":"381-397","source":"Crossref","is-referenced-by-count":19,"title":["Automated verification of the FreeRTOS scheduler in Hip\/Sleek"],"prefix":"10.1007","volume":"16","author":[{"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"first","affiliation":[]},{"given":"Cristian","family":"Gherghina","sequence":"additional","affiliation":[]},{"given":"Guanhua","family":"He","sequence":"additional","affiliation":[]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,18]]},"reference":[{"key":"307_CR1","unstructured":"The SafeRTOS\u2122 project website. http:\/\/www.freertos.org\/safertos.html . Accessed 11 Mar 2014"},{"key":"307_CR2","doi-asserted-by":"crossref","unstructured":"Hoare, T.: The verifying compiler: a grand challenge for computing research. J. ACM 50, 63\u201369 (2003)","DOI":"10.1145\/602382.602403"},{"key":"307_CR3","doi-asserted-by":"crossref","unstructured":"Jones, C., O\u2019Hearn, P., Woodcock, J.: Verified software: a grand challenge. Computer 39, 93\u201395 (2006)","DOI":"10.1109\/MC.2006.145"},{"key":"307_CR4","unstructured":"The FreeRTOS\u2122 project website. http:\/\/www.freertos.org . Accessed 11 Mar 2014"},{"key":"307_CR5","unstructured":"Woodcock, J.: Grand challenge in software verification. In: SBMF (2008)"},{"key":"307_CR6","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL (1999)","DOI":"10.1145\/292540.292552"},{"key":"307_CR7","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)"},{"key":"307_CR8","doi-asserted-by":"crossref","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"WN 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. Computer Progr. 77, 1006\u20131036 (2012)","journal-title":"Sci. Computer Progr."},{"key":"307_CR9","doi-asserted-by":"crossref","unstructured":"Nguyen, H.H., David, C., Qin, S., Chin, W.N.: Automated verification of shape and size properties via separation logic. In: VMCAI (2007)","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"307_CR10","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA version 1.4 user manual (2001)"},{"issue":"6","key":"307_CR11","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011)","journal-title":"J. ACM"},{"key":"307_CR12","doi-asserted-by":"crossref","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: TACAS, pp. 287\u2013302 (2006)","DOI":"10.1007\/11691372_19"},{"key":"307_CR13","doi-asserted-by":"crossref","unstructured":"Chin, W.N., Gherghina, C., Voicu, R., Le, Q.L., Craciun, F., Qin, S.: A specialization calculus for pruning disjunctive predicates to support verification. In: CAV (2011)","DOI":"10.1007\/978-3-642-22110-1_23"},{"key":"307_CR14","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G Klein","year":"2009","unstructured":"Klein, G.: Operating system verification\u2014an overview. Sadhana 34, 27\u201369 (2009)","journal-title":"Sadhana"},{"key":"307_CR15","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI (2003)","DOI":"10.1145\/781131.781153"},{"key":"307_CR16","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"307_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"307_CR18","unstructured":"Sputh, B.H.C., Faust, O., Verhulst, E., Mezhuyev, V.: Opencomrtos: a runtime environment for interacting entities. In: CPA (2009)"},{"key":"307_CR19","doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Formal verification of a microkernel used in dependable software systems. In: SAFECOMP (2009)","DOI":"10.1007\/978-3-642-04468-7_16"},{"key":"307_CR20","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: sel4: formal verification of an os kernel. In: SOSP (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"307_CR21","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, London (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"307_CR22","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO (2005)","DOI":"10.1007\/11804192_6"},{"key":"307_CR23","doi-asserted-by":"crossref","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In: CAV (2008)","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"307_CR24","unstructured":"Magill, S., Tsai, M.H., Lee, P., Tsay, Y.K.: Thor: A tool for reasoning about shape and arithmetic. In: CAV (2008)"},{"key":"307_CR25","unstructured":"M\u00fchlberg, J.T., Leo, F.: Verifying FreeRTOS: from requirements to binary code. In: AVoCS (2011)"},{"key":"307_CR26","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the verifast program verifier. In: APLAS (2010)","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"307_CR27","doi-asserted-by":"crossref","unstructured":"Cook, B., Koskinen, E., Vardi, M.Y.: Temporal property verification as a program analysis task. In: CAV (2011)","DOI":"10.1007\/978-3-642-22110-1_26"},{"key":"307_CR28","doi-asserted-by":"crossref","unstructured":"Qin, S., He, G., Luo, C., Chin, W.N.: Loop invariant synthesis in a combined domain. In: ICFEM (2010)","DOI":"10.1007\/978-3-642-16901-4_31"},{"issue":"0","key":"307_CR29","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1016\/j.jsc.2012.08.007","volume":"50","author":"S Qin","year":"2013","unstructured":"Qin, S., He, G., Luo, C., Chin, W.N., Chen, X.: Loop invariant synthesis in a combined abstract domain. J. Symb. Comput. 50(0), 386\u2013408 (2013)","journal-title":"J. Symb. Comput."},{"key":"307_CR30","doi-asserted-by":"crossref","unstructured":"Qin, S., Luo, C., Chin, W.N., He, G.: Automatically refining partial specifications for program verification. In: FM (2011)","DOI":"10.1007\/978-3-642-21437-0_28"},{"key":"307_CR31","doi-asserted-by":"crossref","unstructured":"Qin, S., He, G., Luo, C., Chin, W.N., Yang, H.: Automatically refining partial specifications for heap-manipulating programs. Sci. Comput Program 82, 56\u201376 (2014)","DOI":"10.1016\/j.scico.2013.03.004"},{"key":"307_CR32","unstructured":"Sharma, A., Hobor, A., Chin, W.N.: Specifying compatible sharing in data structures. In preparation (2013)"},{"key":"307_CR33","doi-asserted-by":"crossref","unstructured":"Lee, O., Yang, H., Petersen, R.: Program analysis for overlaid data structures. In: CAV (2011)","DOI":"10.1007\/978-3-642-22110-1_48"},{"issue":"1","key":"307_CR34","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/s10703-012-0151-7","volume":"41","author":"O Lee","year":"2012","unstructured":"Lee, O., Yang, H., Petersen, R.: A divide-and-conquer approach for analysing overlaid data structures. Formal Methods Syst. Design 41(1), 4\u201324 (2012)","journal-title":"Formal Methods Syst. Design"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0307-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0307-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0307-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T11:04:29Z","timestamp":1565262269000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0307-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,18]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["307"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0307-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,18]]}}}