{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:29:30Z","timestamp":1725564570074},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208037"},{"type":"electronic","value":"9783540246220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_24","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T07:33:53Z","timestamp":1283672033000},"page":"297-308","source":"Crossref","is-referenced-by-count":6,"title":["Applying Jlint to Space Exploration Software"],"prefix":"10.1007","author":[{"given":"Cyrille","family":"Artho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Artho, C.: Finding Faults in Multi-Threaded Programs. Master\u2019s thesis, ETH Z\u00fcrich (2001)"},{"key":"24_CR2","first-page":"68","volume-title":"Proceedings of the 13th ASWEC","author":"C. Artho","year":"2001","unstructured":"Artho, C., Biere, A.: Applying Static Analysis to Large-Scale, Multi-threaded Java Programs. In: Grant, D. (ed.) Proceedings of the 13th ASWEC, pp. 68\u201375. IEEE CS Press, Los Alamitos (2001)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Artho, C., Havelund, K., Biere, A.: High-Level Data Races. In: VVEIS 2003 (April 2003)","DOI":"10.1002\/stvr.281"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstractions for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 268. Springer, Heidelberg (2001)"},{"key":"24_CR5","unstructured":"Benowitz, E.G., Niessner, A.F.: Java for Flight Software. In: Space Mission Challenges for Information Technology (July 2003)"},{"key":"24_CR6","volume-title":"The Real-Time Specification for Java","author":"G. Bollella","year":"2000","unstructured":"Bollella, G., Gosling, J., Brosgol, B., Dibble, P., Furr, S., Turnbull, M.: The Real-Time Specification for Java. Addison-Wesley, Reading (2000)"},{"key":"24_CR7","unstructured":"Brat, G., Giannakopoulou, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., Venet, A., Visser, W.: Experimental Evaluation ofVerification andValidation Tools on Martian Rover Software. In: SEI Software Model Checking Workshop (2003) (Extended abstract)"},{"key":"24_CR8","volume-title":"Proc. 22nd International Conference on Software Engineering","author":"J. Corbett","year":"2000","unstructured":"Corbett, J., Dwyer, M.B., Hatcliff, J., Pasareanu, C.S., Robby, Laubach, S., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proc. 22nd International Conference on Software Engineering, Ireland, ACM Press, New York (2000)"},{"key":"24_CR9","unstructured":"Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended Static Checking. Technical Report 159, Compaq Systems Research Center, Palo Alto, California, USA (1998)"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proc. 24th ACM Symposium on Principles of Programming Languages, France, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"24_CR11","volume-title":"The Java Virtual Language Specification","author":"J. Gosling","year":"2000","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Virtual Language Specification, 2nd edn. Addison Wesley, Reading (2000)","edition":"2"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/10722468_20","volume-title":"SPIN Model Checking and Software Verification","author":"J. Harrow","year":"2000","unstructured":"Harrow, J.: Runtime Checking of Multithreaded Applications with Visual Threads. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 331\u2013342. Springer, Heidelberg (2000)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10722468_15","volume-title":"SPIN Model Checking and Software Verification","author":"K. Havelund","year":"2000","unstructured":"Havelund, K.: Using Runtime Analysis to Guide Model Checking of Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 245\u2013264. Springer, Heidelberg (2000)"},{"key":"24_CR14","unstructured":"Havelund, K., Lowry, M., Park, S., Pecheur, C., Penix, J., Visser, W., White, J.: Formal Analysis of the Remote Agent Before and After Flight. In: 5th NASA Langley Formal Methods Workshop, USA (June 2000)"},{"issue":"4","key":"24_CR15","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. International Journal on Software Tools for Technology Transfer\u00a02(4), 366\u2013381 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"24_CR16","series-title":"ENTCS","volume-title":"Runtime Verification (RV 2001)","author":"K. Havelund","year":"2001","unstructured":"Havelund, K., Ro\u015fu, G.: Monitoring Java Programs with Java Path Explore. In: Havelund, K., Ro\u015fu, G. (eds.) Runtime Verification (RV 2001). ENTCS, vol.\u00a055, Elsevier Science, Amsterdam (2001)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Holzmann, G., Smith, M.: A Practical Method for Verifying Event-Driven Software. In: Proc. ICSE 1999, International Conference on Software Engineering, USA, IEEE\/ACM (1999)","DOI":"10.1145\/302405.302710"},{"key":"24_CR18","volume-title":"Concurrent Programming in Java","author":"D. Lea","year":"1999","unstructured":"Lea, D.: Concurrent Programming in Java, 2nd edn. Addison Wesley, Reading (1999)","edition":"2"},{"key":"24_CR19","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, A.: The Java Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)","edition":"2"},{"key":"24_CR20","unstructured":"Sun Microsystems. Connected, limited device configuration. specification version 1.0a (May 2000), http:\/\/java.sun.com\/j2me\/docs\/"},{"key":"24_CR21","unstructured":"Sun Microsystems. Java 2 documentation, http:\/\/java.sun.com\/j2se\/1.4\/docs\/"},{"issue":"4","key":"24_CR22","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Transactions on Computer Systems\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Transactions on Computer Systems"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/10722468_14","volume-title":"SPIN Model Checking and Software Verification","author":"S.D. Stoller","year":"2000","unstructured":"Stoller, S.D.: Model-Checking Multi-threaded Distributed Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 224\u2013244. Springer, Heidelberg (2000)"},{"key":"24_CR24","volume-title":"Proc. ASE 2000: The 15th IEEE International Conference onAutomated Software Engineering","author":"W. Visser","year":"2000","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Proc. ASE 2000: The 15th IEEE International Conference onAutomated Software Engineering, IEEE CS Press, Los Alamitos (2000)"}],"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\/978-3-540-24622-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T13:41:10Z","timestamp":1559569270000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}