{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:12:58Z","timestamp":1725549178776},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120282"},{"type":"electronic","value":"9783642120299"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12029-9_24","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:56:48Z","timestamp":1268009808000},"page":"338-352","source":"Crossref","is-referenced-by-count":6,"title":["Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups"],"prefix":"10.1007","author":[{"given":"Hermann","family":"Lehner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. In: SS (2004)","DOI":"10.1007\/s10270-004-0058-x"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/3-540-36384-X_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Cata\u00f1o","year":"2002","unstructured":"Cata\u00f1o, N., Huisman, M.: Chase: A static checker for JML\u2019s assignable clause. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 26\u201340. Springer, Heidelberg (2002)"},{"key":"24_CR4","unstructured":"Cheon, Y.: A Runtime Assertion Checker for the Java Modeling Language. PhD thesis, Iowa State University (2003)"},{"key":"24_CR5","unstructured":"ESC\/Java2, http:\/\/secure.ucd.ie\/products\/opensource\/ESCJava2"},{"key":"24_CR6","unstructured":"K\u00e4gi, A., Lehner, H., M\u00fcller, P.: A formalization of JML in the Coq proof system. Technical report, ETH Zurich (2009), http:\/\/www.pm.inf.ethz.ch\/people\/lehnerh\/jmlcoq"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: OOPSLA, pp. 144\u2013153 (1998)","DOI":"10.1145\/286942.286953"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: PLDI, pp. 246\u2013257 (2002)","DOI":"10.1145\/512529.512559"},{"key":"24_CR9","first-page":"89","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 with JML annotations. JLAP\u00a058, 89\u2013106 (2004)","journal-title":"JLAP"},{"key":"24_CR10","unstructured":"Spoto, F., Poll, E.: Static analysis for JML\u2019s assignable clauses. In: Ghelli, G. (ed.) FOOL (2003)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 299\u2013312. Springer, Heidelberg (2001)"},{"key":"24_CR12","unstructured":"Ye, C.: Improving JML\u2019s assignable clause analysis. Technical report, Iowa State University (2006)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12029-9_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:46:54Z","timestamp":1606186014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12029-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120282","9783642120299"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12029-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}