{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T18:51:44Z","timestamp":1773773504977,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540410300","type":"print"},{"value":"9783540452973","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722468_15","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T06:43:32Z","timestamp":1167461012000},"page":"245-264","source":"Crossref","is-referenced-by-count":72,"title":["Using Runtime Analysis to Guide Model Checking of Java Programs"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Bensalem, S., Ganesh, V., Lakhnech, Y., Mu~noz, C., Owre, S., Rue\u00df, H., Rushby, J., Rusu, V., Sa\u00efdi, H., Shankar, N., Singerman, E., Tiwari, A.: An Overview of SAL. In: Proceedings of the 5th NASA Langley Formal Methods Workshop (June 2000)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"15_CR3","unstructured":"Bruening, D.L.: Systematic Testing of Multithreaded Java Programs. Master\u2019s thesis, MIT (1999)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0054175","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Cattel","year":"1998","unstructured":"Cattel, T.: Modeling and Verification of sC++ Applications. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 232. Springer, Heidelberg (1998)"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Corbett, J.: Constructing Compact Models of Concurrent Java Programs. In: Proceedings of the ACM Sigsoft Symposium on Software Testing and Analysis, Clearwater Beach, Florida (1998)","DOI":"10.1145\/271771.271778"},{"key":"15_CR6","volume-title":"Proceedings of the 22nd International Conference on Software Engineering","author":"J. Corbett","year":"2000","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proceedings of the 22nd International Conference on Software Engineering, Limerich, Ireland, June 2000. ACM Press, New York (2000)"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"4","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation Frameworks. Journal of Logic and Computation\u00a04(2), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D., Park, S.: Experience with Predicate Abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"issue":"7","key":"15_CR9","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. Demartini","year":"1999","unstructured":"Demartini, C., Iosif, R., Sist, R.: A Deadlock Detection Tool for Concurrent Java Programs. Software Practice and Experience\u00a029(7), 577\u2013603 (1999)","journal-title":"Software Practice and Experience"},{"key":"15_CR10","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended Static Checking. Technical Report 159, Compaq Systems Research Center, Palo Alto, California, USA (1998)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages, Paris, January 1997, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"15_CR12","volume-title":"The Java Language Specification","author":"J. Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison Wesley, Reading (1996)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: CAV 1997: 6th International Conference on Computer Aided Verification. LNCS, vol.\u00a01254 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Corbett, J.C., Dwyer, M.B., Sokolowski, S., Zheng, H.: A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives. In: Proc. of the 1999 Int. Symposium on Static Analysis (1999)","DOI":"10.1007\/3-540-48294-6_1"},{"key":"15_CR15","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: Proceedings of the 5th NASA Langley Formal Methods Workshop (June 2000)"},{"key":"#cr-split#-15_CR16.1","unstructured":"Havelund, K., Lowry, M., Penix, J.: Formal Analysis of a Space Craft Controller using SPIN. In: Proceedings of the 4th SPIN workshop, Paris, France (November 1998);"},{"key":"#cr-split#-15_CR16.2","unstructured":"To appear in IEEE Transactions of Software Engineering"},{"issue":"4","key":"15_CR17","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 Path- Finder. International Journal on Software Tools for Technology Transfer (STTT)\u00a02(4), 366\u2013381 (2000), Special issue of STTT containing selected submissions to the 4th SPIN workshop, Paris, France (1998)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"K. Havelund","year":"1996","unstructured":"Havelund, K., Shankar, N.: Experiments in Theorem Proving and Model Checking for Protocol Verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 662\u2013681. Springer, Heidelberg (1996)"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-48234-2_17","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"K. Havelund","year":"1999","unstructured":"Havelund, K., Skakkeb\u00e6k, J.: Applying Model Checking in Java Verification. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, p. 216. Springer, Heidelberg (1999)"},{"key":"15_CR20","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, Los Angeles, May 1999, IEEE\/ACM (1999)","DOI":"10.1145\/302405.302710"},{"issue":"5","key":"15_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997), Special issue on Formal Methods in Software Practice","journal-title":"IEEE Trans. on Software Engineering"},{"key":"15_CR22","unstructured":"Iosif, R., Demartini, C., Sisto., R.: Modeling and Validation of JAVA Multithreaded Applications using SPIN. In: Proceedings of the Fourth Workshop on the SPIN Verification System, Paris (November 1998)"},{"key":"15_CR23","unstructured":"JavaClass., http:\/\/www.inf.fu-berlin.de\/~dahm\/JavaClass"},{"issue":"1-2","key":"15_CR24","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0004-3702(98)00068-X","volume":"103","author":"N. Muscettola","year":"1998","unstructured":"Muscettola, N., Nayak, P., Pell, B., Williams, B.: Remote Agent: To Boldly Go Where No AI System Has Gone Before. Artificial Intelligence\u00a0103(1-2), 5\u201348 (1998)","journal-title":"Artificial Intelligence"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Park, D., Stern, U., Dill, D.: Java Model Checking. In: Proc. of the First International Workshop on Automated Program Analysis, Testing and Verification, Limerick, Ireland (June 2000)","DOI":"10.1109\/ASE.2000.873671"},{"issue":"4","key":"15_CR26","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.: 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":"15_CR27","unstructured":"Visual Threads., http:\/\/www.unix.digital.com\/visualthreads\/index.html"},{"key":"15_CR28","unstructured":"Assure., http:\/\/www.kai.com\/assurej"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Java PathFinder - Second Generation of a Java Model Checker. In: Proc. of Post-CAV Workshop on Advances in Verification, Chicago (July 2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"15_CR30","volume-title":"Proc. of ASE 2000: The 15th IEEE International Conference on Automated Software Engineering","author":"W. Visser","year":"2000","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Proc. of ASE 2000: The 15th IEEE International Conference on Automated Software Engineering, September 2000. IEEE CS Press, Los Alamitos (2000)"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Visser, W., Park, S., Penix, J.: Using Predicate Abstraction to Reduce Object- Oriented Programs for Model Checking. In: Proceedings of the 3rd ACM SIGSOFT Workshop on Formal Methods in Software Practice (August 2000)","DOI":"10.1145\/349360.351125"}],"container-title":["Lecture Notes in Computer Science","SPIN Model Checking and Software Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722468_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T03:17:36Z","timestamp":1683688656000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722468_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410300","9783540452973"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/10722468_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}