{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:41:28Z","timestamp":1725565288945},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223429"},{"type":"electronic","value":"9783540278139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_46","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:57:57Z","timestamp":1284440277000},"page":"501-505","source":"Crossref","is-referenced-by-count":51,"title":["Formal Analysis of Java Programs in JavaFAN"],"prefix":"10.1007","author":[{"given":"Azadeh","family":"Farzan","sequence":"first","affiliation":[]},{"given":"Feng","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"46_CR1","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Model checking programs. In: ASE 2000, pp. 3\u201312 (2000)"},{"key":"46_CR2","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.0 Manual (2003), \n \n http:\/\/maude.cs.uiuc.edu\/manual"},{"key":"46_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-44829-2_16","volume-title":"Model Checking Software","author":"S. Eker","year":"2003","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 230\u2013234. Springer, Heidelberg (2003)"},{"key":"46_CR4","unstructured":"Farzan, A., Chen, F., Meseguer, J., Ro\u015fu, G.: JavaFAN. \n \n fsl.cs.uiuc.edu\/es\/javafan"},{"issue":"8","key":"46_CR5","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K. Havelund","year":"2001","unstructured":"Havelund, K., Lowry, M., Penix, J.: Formal Analysis of a Space Craft Controller using SPIN. IEEE Transactions on Software Engineering\u00a027(8), 749\u2013765 (2001); Previous version appeared in Proceedings of the 4th SPIN workshop (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"46_CR6","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Software Tools for Technology Transfer\u00a02(4), 366\u2013381 (2000)","journal-title":"Software Tools for Technology Transfer"},{"key":"46_CR7","unstructured":"Moore, J.S.: \n \n http:\/\/www.cs.utexas.edu\/users\/xli\/prob\/p4\/p4.html"},{"key":"46_CR8","doi-asserted-by":"crossref","unstructured":"Park, D.Y.W., Stern, U., Sakkebaek, J.U., Dill, D.L.: Java model checking. In: ASE 2001, pp. 253\u2013256 (2000)","DOI":"10.1109\/ASE.2000.873671"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_46.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:27:32Z","timestamp":1620012452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}