{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:27:59Z","timestamp":1769750879860,"version":"3.49.0"},"reference-count":19,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2001,10,1]],"date-time":"2001-10-01T00:00:00Z","timestamp":1001894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"vor","delay-in-days":4798,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,10]]},"DOI":"10.1016\/s1571-0661(04)00253-1","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T10:14:39Z","timestamp":1075371279000},"page":"200-217","source":"Crossref","is-referenced-by-count":141,"title":["Monitoring Java Programs with Java PathExplorer"],"prefix":"10.1016","volume":"55","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB1","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB2","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. The Maude system. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), volume 1631 of LNCS, pages 240\u2013243, Trento, Italy, July 1999. Springer-Verlag. System description.","DOI":"10.1007\/3-540-48685-2_18"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB3","unstructured":"S. Cohen. Jtrek. Compaq, http:\/\/www.compaq.com\/java\/download\/jtrek."},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB4","doi-asserted-by":"crossref","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.","DOI":"10.1007\/10722468_19"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB5","unstructured":"B. Fischer, T. Pressburger, G. Rosu, and J. Schumann. The AutoBayes Program Synthesis System - System Description. In Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2001), Siena, Italy, June 2001."},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB6","doi-asserted-by":"crossref","unstructured":"J. Harrow. Runtime Checking of Multithreaded Applications with Visual Threads. In SPIN Model Checking and Software Verification, volume 1885 of LNCS, pages 331\u2013342. Springer, 2000.","DOI":"10.1007\/10722468_20"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB7","doi-asserted-by":"crossref","unstructured":"K. Havelund. Using Runtime Analysis to Guide Model Checking of Java Programs. In SPIN Model Checking and Software Verification, volume 1885 of LNCS, pages 245\u2013264. Springer, 2000.","DOI":"10.1007\/10722468_15"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB8","unstructured":"K. Havelund, M. Lowry, and J. Penix. Formal Analysis of a Space Craft Controller using SPIN. In Proceedings of the 4th SPIN workshop, Paris, France, November 1998. To appear in IEEE Transactions of Software Engineering."},{"issue":"4","key":"10.1016\/S1571-0661(04)00253-1_NEWBIB9","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","article-title":"Model Checking Java Programs using Java PathFindeir","volume":"2","author":"Havelund","year":"1998","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB10","unstructured":"K. Havelund and G. Ro\u015fu. Testing Linear Temporal Logic Formulae on Finite Execution Traces. RIACS Technical report, http:\/\/ase.arc.nasa.gov\/pax, November 2000."},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB11","unstructured":"K. Havelund and G. Ro\u015fu. Java PathExplorer \u2013 A Runtime Verification Tool. In Proceedings of the 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space (i-SAIRAS'01), Montreal, Canada, June 2001."},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB12","unstructured":"J. Hsiang. Refutational Theorem Proving using Term Rewriting Systems. PhD thesis, University of Illinois at Champaign-Urbana, 1981."},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB13","unstructured":"I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan. Runtime Assurance Based on Formal Specifications. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999."},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB14","doi-asserted-by":"crossref","unstructured":"M. Lowry, A. Philpot, T. Pressburger, I. Underwood, R. Waldinger, and M. Stickel. Amphion: Automatic Programming for the NAIF Toolkit. In NASA Science Information Systems Newsletter, volume 31, February 1994.","DOI":"10.1109\/KBSE.1994.342685"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB15","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.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB16","unstructured":"G. Ro\u015fu and K. Havelund. Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae. RIACS Technical report, http:\/\/ase.arc.nasa.gov\/pax, January 2001."},{"issue":"4","key":"10.1016\/S1571-0661(04)00253-1_NEWBIB17","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1145\/265924.265927","article-title":"Eraser: A Dynamic Data Race Detector for Multithreaded Programs","volume":"15","author":"Savage","year":"1997","journal-title":"ACM Transactions on Computer Systems"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB18","doi-asserted-by":"crossref","unstructured":"W. Visser, K. Havelund, G. Brat, and S. Park. Model Checking Programs. In Proceedings of ASE'2000: The 15th IEEE International Conference on Automated Software Engineering. IEEE CS Press, September 2000.","DOI":"10.1109\/ASE.2000.873645"},{"key":"10.1016\/S1571-0661(04)00253-1_NEWBIB19","doi-asserted-by":"crossref","unstructured":"J. Whittle and J. Schumann. Generating Statechart Designs From Scenarios. In International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, June 2000.","DOI":"10.1145\/337180.337217"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002531?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002531?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T12:26:56Z","timestamp":1585484816000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104002531"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,10]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,10]]}},"alternative-id":["S1571066104002531"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00253-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,10]]}}}