{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T10:10:03Z","timestamp":1746439803354,"version":"3.40.4"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319124650"},{"type":"electronic","value":"9783319124667"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12466-7_7","type":"book-chapter","created":{"date-parts":[[2014,10,22]],"date-time":"2014-10-22T04:44:58Z","timestamp":1413953098000},"page":"110-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning About Resources in the Embedded Systems Language Hume"],"prefix":"10.1007","author":[{"given":"Hans-Wolfgang","family":"Loidl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gudmund","family":"Grov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,22]]},"reference":[{"issue":"3","key":"7_CR1","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/j.tcs.2007.09.003","volume":"389","author":"D Aspinall","year":"2007","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resources. Theoret. Comput. Sci. 389(3), 411\u2013445 (2007)","journal-title":"Theoret. Comput. Sci."},{"issue":"2\u20133","key":"7_CR2","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/j.tcs.2004.07.036","volume":"335","author":"JCM Baeten","year":"2005","unstructured":"Baeten, J.C.M.: A brief history of process algebra. Theoret. Comput. Sci. 335(2\u20133), 131\u2013146 (2005)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"7_CR3","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/PL00003930","volume":"12","author":"MJ Butler","year":"2000","unstructured":"Butler, M.J.: csp2B: a practical approach to combining CSP and B. Form. Asp. Comput. 12(3), 182\u2013198 (2000)","journal-title":"Form. Asp. Comput."},{"key":"7_CR4","unstructured":"Filli\u00e2tre, J.-C.: Why: a multi-language multi-prover verification tool. Research report 1366, LRI, Universit\u00e9 Paris Sud, March 2003"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Fischer, C.: CSP-OZ: a combination of object-Z and CSP. In: Formal Methods for Open Object-Based Distributed Systems (FMOODS \u201997), pp. 423\u2013438 (1997)","DOI":"10.1007\/978-0-387-35261-9_29"},{"key":"7_CR6","unstructured":"Grov, G.: Reasoning about correctness properties of a coordination programming language. Ph.D. thesis, Heriot-Watt University (2009)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Grov, G., Michaelson, G., Ireland, A.: Formal verification of concurrent scheduling strategies using TLA. In: International Conference on Parallel and Distributed Systems (ICPADS\u201907), pp. 1\u20136. IEEE, Hsinchu, December 2007","DOI":"10.1109\/ICPADS.2007.4447839"},{"key":"7_CR8","unstructured":"Grov, G., Merz, S.: A Definitional Encoding of TLA* in Isabelle\/Hol. Archive of Formal Proofs, Formal proof development, November 2011. http:\/\/afp.sf.net\/entries\/TLA"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-39815-8_3","volume-title":"Generative Programming and Component Engineering","author":"K Hammond","year":"2003","unstructured":"Hammond, K., Michaelson, G.J.: Hume: a domain-specific language for real-time embedded systems. In: Pfenning, F., Macko, M. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 37\u201356. Springer, Heidelberg (2003)"},{"key":"7_CR10","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 284. Springer, Heidelberg (2000)"},{"key":"7_CR12","volume-title":"Systematic Software Development Using VDM","author":"C Jones","year":"1990","unstructured":"Jones, C.: Systematic Software Development Using VDM. Prentice Hall, Englewood Cliffs (1990)"},{"key":"7_CR13","unstructured":"Kleymann, T.: Hoare logic and VDM: machine-checked soundness and completeness proofs. Ph.D. thesis, LFCS, University of Edinburgh (1999)"},{"issue":"3","key":"7_CR14","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-30142-4_15","volume-title":"Theorem Proving in Higher Order Logics","author":"J Longley","year":"2004","unstructured":"Longley, J., Pollack, R.: Reasoning about CBV functional programs in Isabelle\/HOL. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 201\u2013216. Springer, Heidelberg (2004)"},{"issue":"1\u20132","key":"7_CR16","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The krakatoa tool for certification of Java\/JavaCard programs annotated in JML. J. Logic Algebraic Program. 58(1\u20132), 89\u2013106 (2004)","journal-title":"J. Logic Algebraic Program."},{"key":"7_CR17","unstructured":"M\u00fcller, P., Meyer, J., Poetzsch-Heffter, A.: Programming and interface specification language of JIVE. Fernuniversit\u00e4t Hagen, Technical report (2000)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45793-3_8","volume-title":"Computer Science Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, p. 103. Springer, Heidelberg (2002)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.O.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, p. 162. Springer, Heidelberg (1999)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Symposium on Logic in Computer Science (LICS\u201902), pp. 55\u201374. IEEE Computer Society, Copenhagen, July 2002","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"4","key":"7_CR21","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/s00165-005-0076-7","volume":"17","author":"S Schneider","year":"2005","unstructured":"Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Form. Asp. Comput. Appl. Form. Methods 17(4), 390\u2013422 (2005)","journal-title":"Form. Asp. Comput. Appl. Form. Methods"},{"issue":"13","key":"7_CR22","doi-asserted-by":"publisher","first-page":"1173","DOI":"10.1002\/cpe.598","volume":"13","author":"D von Oheimb","year":"2001","unstructured":"von Oheimb, D.: Hoare logic for Java in Isabelle\/HOL. Concurr. Comput. Pract. Exp. 13(13), 1173\u20131214 (2001)","journal-title":"Concurr. Comput. Pract. Exp."}],"container-title":["Lecture Notes in Computer Science","Foundational and Practical Aspects of Resource Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12466-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T09:39:01Z","timestamp":1746437941000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12466-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319124650","9783319124667"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12466-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"22 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}