{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T05:40:01Z","timestamp":1746164401694,"version":"3.40.4"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,3,28]],"date-time":"2014-03-28T00:00:00Z","timestamp":1395964800000},"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-0306-5","type":"journal-article","created":{"date-parts":[[2014,3,27]],"date-time":"2014-03-27T05:51:32Z","timestamp":1395899492000},"page":"363-380","source":"Crossref","is-referenced-by-count":3,"title":["Expressive program verification via structured specifications"],"prefix":"10.1007","volume":"16","author":[{"given":"Cristian","family":"Gherghina","sequence":"first","affiliation":[]},{"given":"Cristina","family":"David","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,28]]},"reference":[{"key":"306_CR1","unstructured":"The FreeRTOS $$^{{\\rm TM}}$$ TM project website. (2013). URL: http:\/\/www.freertos.org"},{"key":"306_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: CASSIS, vol. 3362, pp. 49\u201369. Springer-Verlag, LNCS, New York (2004)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"306_CR3","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: FMCO, Springer LNCS 4111, pp. 115\u2013137 (2006)","DOI":"10.1007\/11804192_6"},{"key":"306_CR4","doi-asserted-by":"crossref","unstructured":"Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: FMCAD, pp. 275\u2013293 (1996)","DOI":"10.1007\/BFb0031816"},{"key":"306_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"306_CR6","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Trans. 7(3), 212\u2013232 (2005)"},{"key":"306_CR7","doi-asserted-by":"crossref","unstructured":"Chang, B.Y.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247\u2013260 (2008)","DOI":"10.1145\/1328897.1328469"},{"key":"306_CR8","doi-asserted-by":"crossref","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Multiple pre\/post specifications for heap-manipulating methods. In: HASE, pp. 357\u2013364 (2007)","DOI":"10.1109\/HASE.2007.19"},{"issue":"9","key":"306_CR9","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. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"306_CR10","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"306_CR11","unstructured":"Ferreira, J.F., Gherghina, C., He, G., Qin, S., Chin, W.-N.: Automated verification of the FreeRTOS scheduler in HIP\/SLEEK. Int. J. Softw. Tools Technol. Trans (2014). doi: 10.1007\/s10009-014-307-4"},{"key":"306_CR12","doi-asserted-by":"crossref","unstructured":"Gherghina, C., David, C., Qin, S., Chin, W.N.: Structured specifications for better verification of heap-manipulating programs. In: FM (2011)","DOI":"10.1007\/978-3-642-21437-0_29"},{"key":"306_CR13","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: POPL, pp. 14\u201326. London (2001)","DOI":"10.1145\/373243.375719"},{"key":"306_CR14","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the veriFast program verifier. In: APLAS, pp. 304\u2013311 (2010)","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"306_CR15","doi-asserted-by":"crossref","unstructured":"Jonkers, H.B.M.: Upgrading the pre- and postcondition technique. In: VDM, pp. 428\u2013456. Springer-Verlag, London (1991)","DOI":"10.1007\/3-540-54834-3_26"},{"key":"306_CR16","unstructured":"Klarlund, N., Moller, A.: MONA Version 1.4-User Manual. BRICS Notes Series (2001). URL: http:\/\/citeseer.ifi.unizh.ch\/klarlund01mona.html"},{"key":"306_CR17","volume-title":"A Specification Logic for Termination and Non-Termination Reasoning Tech. rep","author":"TC Le","year":"2012","unstructured":"Le, T.C., Gherghina, C., Hobor, A., Chin, W.N.: A Specification Logic for Termination and Non-Termination Reasoning Tech. rep. National University of Singapore, Singapore (2012)"},{"key":"306_CR18","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L.: Enhancing the pre- and postcondition technique for more expressive specifications. In: FM (1999)","DOI":"10.1007\/3-540-48118-4_8"},{"key":"306_CR19","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR (Dakar), pp. 348\u2013370 (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"306_CR20","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL, pp. 247\u2013258 (2005)","DOI":"10.1145\/1047659.1040326"},{"key":"306_CR21","doi-asserted-by":"crossref","unstructured":"Nguyen, H., David, C., Qin, S., Chin, W.: Automated verification of shape and size properties via separation logic. In: VMCAI. Nice, France (2007)","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"306_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: POPL, Venice, Italy (2004)","DOI":"10.1145\/964001.964024"},{"key":"306_CR23","unstructured":"Pientka, B.: A heuristic for case analysis. Undergraduate thesis, Technical Paper 37, Department of Artificial Intelligence, University of Edinburgh (1995)"},{"key":"306_CR24","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega Test: A fast practical integer programming algorithm for dependence analysis. Commun. ACM 8, 102\u2013114 (1992)","DOI":"10.1145\/135226.135233"},{"key":"306_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. Copenhagen, Denmark (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"306_CR26","doi-asserted-by":"crossref","unstructured":"Seino, T., Ogato, K., Futatsugi, K.: Mechanically supporting case analysis for verification of distributed systems. IJPCC (2005)","DOI":"10.1108\/17427370580000119"},{"key":"306_CR27","unstructured":"Woodcock, J.: Grand challenge in software verification. In: SBMF (2008)"},{"key":"306_CR28","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: An integrated proof language for imperative programs. In: PLDI, pp. 338\u2013351. ACM, New York (2009)","DOI":"10.1145\/1543135.1542514"}],"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-0306-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0306-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0306-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T05:17:42Z","timestamp":1746163062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0306-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,28]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["306"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0306-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,3,28]]}}}