{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:34:05Z","timestamp":1725496445058},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540003489"},{"type":"electronic","value":"9783540363842"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36384-x_6","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:21:13Z","timestamp":1196328073000},"page":"26-40","source":"Crossref","is-referenced-by-count":15,"title":["CHASE:A Static Checker for JML\u2019s Assignable Clause"],"prefix":"10.1007","author":[{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"first","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"D. Bartetzko, C. Fischer, M. M\u00f6ller, and H. Wehrheim. Jass \u2014 Java with Assertions. In K. Havelund and G. Ros\u015fu, editors, ENTCS, volume 55(2). Elsevier Publishing, 2001.","DOI":"10.1016\/S1571-0661(04)00247-6"},{"key":"6_CR2","series-title":"Lect Notes Comput Sci","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 (TACAS 2001)","author":"J. Berg van den","year":"2001","unstructured":"J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), number 2031 in LNCS, pages 299\u2013312. Springer, 2001."},{"issue":"10","key":"6_CR3","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.469460","volume":"21","author":"A. Borgida","year":"1995","unstructured":"A. Borgida, J. Mylopoulos, and R. Reiter. On the frame problem in procedure specifications. IEEE Transactions on Software Engineering, 21(10):785\u2013798, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR4","unstructured":"N. Cata\u00f1o and M. Huisman. Assignable specifications for the Electronic Purse case study, 2002. http:\/\/www-sop.inria.fr\/lemme\/verificard\/modifSpec ."},{"key":"6_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-45614-7_16","volume-title":"Formal Methods Europe (FME\u2019 02)","author":"N. Cata\u00f1o","year":"2002","unstructured":"N. Cata\u00f1o and M. Huisman. Formal specification and static checking of Gemplus\u2019s electronic purse using ESC\/Java. In L.-H. Eriksson and P.A. Lindsay, editors, Formal Methods Europe (FME\u2019 02), number 2391 in LNCS, pages 272\u2013289. Springer, 2002."},{"key":"6_CR6","unstructured":"Differences between Esc\/Java and JML, 2000. Comes with JML distribution, in file esc-jml-diffs.txt."},{"key":"6_CR7","unstructured":"J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification Second Edition. The Java Series. Addison-Wesley, 2000."},{"key":"6_CR8","unstructured":"The JASS project. http:\/\/semantik.informatik.uni-oldenburg.de\/~jass\/ ."},{"key":"6_CR9","unstructured":"G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary Design of JML: a Behavioral Interface Specification Language for Java. Technical Report 98-06, Iowa State University, Department of Computer Science, 1998. http:\/\/www.cs.iastate.edu\/~leavens\/JML\/prelimdesign\/ ."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"K.R.M. Leino. Data groups: specifying the modification of extended state. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA\u2019 98), pages 144\u2013153. ACM Press, 1998.","DOI":"10.1145\/286936.286953"},{"key":"6_CR11","series-title":"Lect Notes Comput Sci","first-page":"185","volume-title":"Static Analysis (SAS 2001)","author":"K.R.M. Leino","year":"2001","unstructured":"K.R.M. Leino. Applications of Extended Static Checking. In P. Cousot, editor, Static Analysis (SAS 2001), number 2126 in LNCS, pages 185\u2013193. Springer, 2001."},{"key":"6_CR12","unstructured":"K.R.M. Leino, G. Nelson, and J.B. Saxe. ESC\/Java user\u2019s manual. Technical Report SRC 2000-002, Compaq System Research Center, 2000."},{"issue":"1","key":"6_CR13","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B.H. Liskov","year":"1994","unstructured":"B.H. Liskov and J.M. Wing. A behavioral notion of subtyping. ACM Trans. on Progr. Lang. and Systems, 16(1):1811\u20131841, 1994.","journal-title":"ACM Trans. on Progr. Lang. and Systems"},{"key":"6_CR14","unstructured":"The LOOP project. http:\/\/www.cs.kun.nl\/~bart\/LOOP\/ ."},{"key":"6_CR15","unstructured":"J. McCarthy and P. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 463\u2013502. Edinburgh Univ. Press, 1969."},{"key":"6_CR16","unstructured":"B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"P. M\u00fcller. Modular Specification and Veri.cation of Object Oriented Programs. PhD thesis, FernUniversit\u00e4t Hagen, 2001.","DOI":"10.1007\/3-540-45651-1"},{"key":"6_CR18","unstructured":"E. Poll and F. Spoto. Static analysis for JML\u2019s assignable clauses, 2002. Manuscript."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36384-X_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T04:54:59Z","timestamp":1557032099000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36384-X_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12,16]]},"ISBN":["9783540003489","9783540363842"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-36384-x_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002,12,16]]}}}