{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:02:32Z","timestamp":1784232152400,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540006244","type":"print"},{"value":"9783540364986","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36498-6_5","type":"book-chapter","created":{"date-parts":[[2007,6,7]],"date-time":"2007-06-07T18:28:14Z","timestamp":1181240894000},"page":"87-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Experiments with Test Case Generation and Runtime Analysis"],"prefix":"10.1007","author":[{"given":"Cyrille","family":"Artho","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Doron","family":"Drusinksy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Allen","family":"Goldberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mike","family":"Lowry","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Corina","family":"Pasareanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2003,3,14]]},"reference":[{"key":"5_CR1","unstructured":"S. Bensalem and K. Havelund. Reducing False Positives in Runtime Analysis of Deadlocks. Submitted for publication, October 2002. 91, 93, 95"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated Testing Based on Java Predicates. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), July 2002. 90","DOI":"10.1145\/566189.566191"},{"key":"5_CR3","unstructured":"G. Brat, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, and W. Visser. A Comparative Field Study of Advanced Verification Technologies. Internal report, in preparation for submission, November 2002. 87, 95"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"M. Clavel, F. J. Dur\u00e1n, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, and J. F. Quesada. Maude: Specification and Programming in Rewriting Logic, March 1999. Maude System documentation at maude.csl.sri.com\/papers. 94","DOI":"10.1007\/3-540-48685-2_18"},{"key":"5_CR5","unstructured":"S. Cohen. Jtrek. Compaq, http:\/\/www.compaq.com\/java\/download\/jtrek . 92"},{"key":"5_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/10722468_19","volume-title":"SPIN Model Checking and Software Verification","author":"D. Drusinsky","year":"2000","unstructured":"D. Drusinsky. The Temporal Rover and the ATG Rover. In SPIN Model Checking and Software Verification, volume 1885 of LNCS, pages 323\u2013330. Springer, 2000. 89, 91, 93, 94"},{"key":"5_CR7","unstructured":"D. Drusinsky. Monitoring Temporal Rules with Temporal Data. Submitted for publication, October 2002. 94"},{"key":"5_CR8","unstructured":"M. Feather, S. Fickas, and N. Razermera-Mamy. Model-Checking for Validation of a Fault Protection System. In Proceedings of Sixth IEEE International Symposium on High Assurance System Engineering. IEEE Computer Society, October 2001. 103"},{"key":"5_CR9","unstructured":"E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns-Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995. 92"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"W. Grieskamp, Y. Gurevich, W. Schulte, and M. Veanes. Generating Finite State Machines from Abstract State Machines. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), July 2002. 89","DOI":"10.1145\/566189.566190"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"A. Groce and W. Visser. Model Checking Java Programs using Structural Heuristics. In Proceedings of the 2002 International Symposium on Software Testing and Analysis (ISSTA). ACM Press, July 2002. 90","DOI":"10.1145\/566173.566175"},{"key":"5_CR12","unstructured":"A. Hartman. Model Based Test Generation Tools. http:\/\/www.agedis.de\/documents\/ModelBasedTestGenerationToolsc s.pdf+ .89"},{"key":"5_CR13","unstructured":"K. Havelund, S. Johnson, and G. Ro\u015fu. Specification and Error Pattern Based Program Monitoring. In Proceedings of the European Space Agency workshop on On-Board Autonomy, Noordwijk, The Netherlands, October 2001. 95"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"K. Havelund and G. Ro\u015fu. Monitoring Java Programs with Java PathExplorer. In K. Havelund and G. Ro\u015fu, editors, Proceedings of the First International Workshop on Runtime Verification (RV\u201901), volume 55 of Electronic Notes in Theoretical Computer Science, pages 97\u2013114, Paris, France, July 2001. Elsevier Science. 91, 93","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"K. Havelund and G. Ro\u015fu. Monitoring Programs using Rewriting. In Proceedings of the International Conference on Automated Software Engineering (ASE\u201901), pages 135\u2013143. IEEE CS Press, 2001. Coronado Island, California. 95","DOI":"10.1109\/ASE.2001.989799"},{"key":"5_CR16","unstructured":"K. Havelund and G. Ro\u015fu. A Rewriting-based Approach to Trace Analysis. Submitted for journal publication, September 2002. 95"},{"key":"5_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201902)","author":"K. Havelund","year":"2002","unstructured":"K. Havelund and G. Ro\u015fu. Synthesizing Monitors for Safety Properties. In Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201902), volume 2280 of Lecture Notes in Computer Science, pages 342\u2013356. Springer, 2002. EASST best paper award at ETAPS\u201902. 95"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"H. Hong, I. Lee, O. Sokolsky, and H. Ural. A Temporal Logic Based Theory of Test Coverage and Generation. In Proceedings of the 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2002. 90","DOI":"10.1007\/3-540-46002-0_23"},{"issue":"7","key":"5_CR19","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J. C. King","year":"1976","unstructured":"J. C. King. Symbolic Execution and Program Testing. Communications of the ACM, 19(7):385\u2013394, 1976. 89","journal-title":"Communications of the ACM"},{"issue":"8","key":"5_CR20","doi-asserted-by":"publisher","first-page":"870","DOI":"10.1109\/32.57624","volume":"16","author":"B. Korel","year":"1990","unstructured":"B. Korel. Automated Software Test Data Generation. IEEE Transaction on Software Engineering, 16(8):870\u2013879, August 1990. 89","journal-title":"IEEE Transaction on Software Engineering"},{"key":"5_CR21","unstructured":"Parasoft. http:\/\/www.parasoft.com . 89"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46\u201377, 1977. 93","DOI":"10.1109\/SFCS.1977.32"},{"issue":"4","key":"5_CR23","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Transactions on Computer Systems, 15(4):391\u2013411, November 1997. 95","journal-title":"ACM Transactions on Computer Systems"},{"key":"5_CR24","unstructured":"N. Tracey, J. Clark, and K. Mander. The Way Forward for Unifying Dynamic Test-Case Generation: The Optimisation-Based Approach. In International Workshop on Dependable Computing and Its Applications (DCIA), pages 169\u2013180. IFIP, January 1998. 89"},{"key":"5_CR25","unstructured":"T-VEC. http:\/\/www.t-vec.com . 89"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"W. Visser, K. Havelund, G. Brat, and S. Park. Model Checking Programs. In Proceedings of ASE\u20192000: The 15th IEEE International Conference on Automated Software Engineering. IEEE CS Press, September 2000. 90","DOI":"10.1109\/ASE.2000.873645"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines 2003"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36498-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T01:56:10Z","timestamp":1737078970000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36498-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540006244","9783540364986"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-36498-6_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"14 March 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}