{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:12:41Z","timestamp":1770750761928,"version":"3.50.0"},"publisher-location":"Berlin, Heidelberg","reference-count":63,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540691471","type":"print"},{"value":"9783540691495","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_40","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"374-383","source":"Crossref","is-referenced-by-count":65,"title":["Verify Your Runs"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Allen","family":"Goldberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"40_CR1","unstructured":"1st \u2013 5th Workshops on Runtime Verification (RV 2001 - RV 2005). ENTCS, vol.\u00a055(2), 70(4), 89(2), 113. Elsevier Science Direct. Amsterdam (to be published, 2001\u20132005), http:\/\/www.runtime-verification.org"},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"Allan, C., Avgustinov, P., Kuzins, S., de Moor, O., Sereni, D., Sittamplan, G., Tibble, J., Christensen, A.S., Hendren, L., Lhot\u00e1k, O.: Adding Trace Matching with Free Variables to AspectJ. In: OOPSLA 2005 (2005)","DOI":"10.1145\/1094811.1094839"},{"issue":"2\u20133","key":"40_CR3","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.tcs.2004.11.007","volume":"336","author":"C. Artho","year":"2005","unstructured":"Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M., Pasareanu, C., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining Test-Case Generation and Runtime Verification. Theoretical Computer Science\u00a0336(2\u20133), 209\u2013234 (2005), Extended version of [4]","journal-title":"Theoretical Computer Science"},{"key":"40_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-36498-6_5","volume-title":"Abstract State Machines 2003. Advances in Theory and Practice","author":"C. Artho","year":"2003","unstructured":"Artho, C., Drusinsky, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., Ro\u015fu, G., Visser, W.: Experiments with Test Case Generation and Runtime Analysis. In: B\u00f6rger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol.\u00a02589, pp. 87\u2013107. Springer, Heidelberg (2003)"},{"key":"40_CR5","doi-asserted-by":"crossref","unstructured":"Artho, C., Havelund, K., Biere, A.: High-Level Data Races. Software Testing, Verification and Reliability\u00a013(4) (2004)","DOI":"10.1002\/stvr.281"},{"key":"40_CR6","doi-asserted-by":"crossref","unstructured":"Artho, C., Havelund, K., Biere, A.: Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. In: 2nd International Symposium on Automated Technology for Verification and Analysis, Taiwan, October\u2013November (2004)","DOI":"10.1007\/978-3-540-30476-0_16"},{"key":"40_CR7","unstructured":"ASML. http:\/\/research.microsoft.com\/fse\/asml"},{"key":"40_CR8","unstructured":"AspectJ. http:\/\/eclipse.org\/aspectj"},{"key":"40_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M.\u00ca. Barnett\u00ca","year":"2005","unstructured":"Barnett\u00ca, M.\u00ca., Leino, K.R.M.\u00ca., Schulte, W.\u00ca.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, Springer, Heidelberg (2005)"},{"key":"40_CR10","doi-asserted-by":"crossref","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program Monitoring with LTL in Eagle. In: Parallel and Distributed Systems: Testing and Debugging (PADTAD 2004), Santa Fee, New Mexico, USA, April (2004)","DOI":"10.1109\/IPDPS.2004.1303336"},{"key":"40_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H. Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, Springer, Heidelberg (2004)"},{"key":"40_CR12","unstructured":"BCEL. http:\/\/jakarta.apache.org\/bcel"},{"key":"40_CR13","unstructured":"Bensalem, S., Bozga, M., Krichen, M., Tripakis, S.: Testing Conformance of Real-Time Applications by Automatic Generation of Observers. In: Proceedings of the 4th International Workshop on Runtime Verification (RV 2004) [1], pp. 19\u201338 (2004)"},{"key":"40_CR14","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Fernandez, J.-C., Havelund, K., Mounier, L.: Confirmation of Deadlock Potentials Detected by Runtime Analysis. In: Parallel and Distributed Systems: Testing and Debugging (PADTAD 2006), Portland, Maine, USA (July 2006)","DOI":"10.1145\/1147403.1147412"},{"key":"40_CR15","unstructured":"Bensalem, S., Havelund, K.: Scalable Dynamic Deadlock Analysis of Multi-Threaded Programs. In: Parallel and Distributed Systems: Testing and Debugging (PADTAD - 3), IBM Verification Conference, Haifa, Israel, November 2005. LNCS (2005)"},{"key":"40_CR16","unstructured":"Chen, F., D\u2019Amorim, M., Ro\u015fu, G.: Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP. In: Proceedings of the 5th International Workshop on Runtime Verification (RV 2005) [1] (2005)"},{"key":"40_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-48685-2_18","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"1999","unstructured":"Clavel, M., Dur\u00e1n, F.J., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: The Maude System. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 240\u2013243. Springer, Heidelberg (1999)"},{"key":"40_CR18","unstructured":"Daikon. http:\/\/pag.csail.mit.edu\/daikon"},{"key":"40_CR19","unstructured":"D\u2019Amorim, M., Havelund, K.: Runtime Verification for Java. In: Workshop on Dynamic Program Analysis (WODA 2005) (March 2005)"},{"key":"40_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"M. D\u2019Amorim","year":"2005","unstructured":"D\u2019Amorim, M., Rosu, G.: Efficient Monitoring of Omega-Languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"key":"40_CR21","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: Runtime Monitoring of Synchronous Systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166\u2013174 (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"40_CR22","series-title":"Lecture Notes in Computer Science","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":"Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 323\u2013330. Springer, Heidelberg (2000)"},{"key":"40_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-45069-6_11","volume-title":"Computer Aided Verification","author":"D. Drusinsky","year":"2003","unstructured":"Drusinsky, D.: Monitoring Temporal Rules Combined with Time Series. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 114\u2013118. Springer, Heidelberg (2003)"},{"key":"40_CR24","unstructured":"Drusinsky, D.: Semantics and Runtime Monitoring of TLCharts: Statechart Automata with Temporal Logic Conditioned Transitions. In: Proceedings of the 4th International Workshop on Runtime Verification (RV 2004) [1], pp. 2\u201318 (2004)"},{"key":"40_CR25","unstructured":"Eiffel. http:\/\/www.eiffel.com"},{"key":"40_CR26","unstructured":"Eytani, Y., Havelund, K., Stoller, S., Ur, S.: Toward a Framework and Benchmark for Testing Tools for Multi-Threaded Programs. In: Concurrency and Computation: Practice and Experience (to appear, 2005)"},{"key":"40_CR27","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting Statistics over Runtime Executions. In: Proceedings of the 2nd International Workshop on Runtime Verification (RV 2002) [1], pp. 36\u201355 (2002)","DOI":"10.1016\/S1571-0661(04)80576-0"},{"key":"40_CR28","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Sipma, H.: Checking Finite Traces using Alternating Automata. In: Proceedings of the 1st International Workshop on Runtime Verification (RV 2001)[1], pp. 44\u201360 (2001)","DOI":"10.1016\/S1571-0661(04)00250-6"},{"issue":"1","key":"40_CR29","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/982962.964023","volume":"39","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C., Freund, S.: Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs. SIGPLAN Not.\u00a039(1), 256\u2013267 (2004)","journal-title":"SIGPLAN Not."},{"key":"40_CR30","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Havelund, K.: Automata-Based Verification of Temporal Properties on Running Programs. In: Proceedings, International Conference on Automated Software Engineering (ASE 2001), Coronado Island, California. ENTCS, pp. 412\u2013416 (2001)","DOI":"10.1109\/ASE.2001.989841"},{"key":"40_CR31","unstructured":"Goldberg, A., Havelund, K.: Instrumentation of Java Bytecode for Runtime Analysis. In: Fifth ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP 2003), Darmstadt, Germany (July 2003)"},{"key":"40_CR32","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A Visual Formalism For Complex Systems. Science of Computer Programming\u00a08, 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"40_CR33","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":"40_CR34","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":"40_CR35","unstructured":"Havelund, K., Ro\u015fu, G.: Monitoring Java Programs with Java PathExplorer. In: Proceedings of the 1st International Workshop on Runtime Verification (RV 2001)[1], pp. 97\u2013114 (2001)"},{"key":"40_CR36","doi-asserted-by":"crossref","unstructured":"Havelund, K., Ro\u015fu, G.: Monitoring Programs using Rewriting. In: Proceedings, International Conference on Automated Software Engineering (ASE 2001), Coronado Island, California. Institute of Electrical and Electronics Engineers, pp. 135\u2013143 (2001)","DOI":"10.1109\/ASE.2001.989799"},{"key":"40_CR37","doi-asserted-by":"crossref","unstructured":"Havelund, K., Ro\u015fu, G.: An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design\u00a024(2) (March 2004)","DOI":"10.1023\/B:FORM.0000017721.39909.4b"},{"issue":"2","key":"40_CR38","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K. Havelund","year":"2004","unstructured":"Havelund, K., Ro\u015fu, G.: Efficient Monitoring of Safety Properties. Software Tools for Technology Transfer\u00a06(2), 158\u2013173 (2004)","journal-title":"Software Tools for Technology Transfer"},{"key":"40_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002), Best paper award"},{"key":"40_CR40","unstructured":"Jass. http:\/\/csd.informatik.uni-oldenburg.de\/~jass"},{"key":"40_CR41","unstructured":"JML. http:\/\/www.cs.iastate.edu\/~leavens\/JML"},{"key":"40_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"G. Kiczales","year":"2001","unstructured":"Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An Overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 327\u2013353. Springer, Heidelberg (2001)"},{"key":"40_CR43","unstructured":"Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a Run-time Assurance Tool for Java. In: Proceedings of the 1st International Workshop on Runtime Verification (RV 2001)[1] (2001)"},{"key":"40_CR44","unstructured":"Larch. http:\/\/www.cs.iastate.edu\/larch-faq-webboy.html"},{"key":"40_CR45","unstructured":"Patterns. http:\/\/patterns.projects.cis.ksu.edu"},{"key":"40_CR46","unstructured":"PSL\/Sugar. http:\/\/www.pslsugar.org"},{"key":"40_CR47","unstructured":"PVS. http:\/\/pvs.csl.sri.com"},{"key":"40_CR48","unstructured":"RAISE. http:\/\/spd-web.terma.com\/Projects\/RAISE"},{"issue":"2","key":"40_CR49","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G. Ro\u015fu","year":"2005","unstructured":"Ro\u015fu, G., Havelund, K.: A Rewriting-based Approach to Trace Analysis. Automated Software Engineering\u00a012(2), 151\u2013197 (2005)","journal-title":"Automated Software Engineering"},{"issue":"4","key":"40_CR50","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":"40_CR51","unstructured":"Sen, K., Ro\u015fu, G.: Generating Optimal Monitors for Extended Regular Expressions. In: Proceedings of the 3rd International Workshop on Runtime Verification (RV 2003)[1], pp. 162\u2013181 (2003)"},{"key":"40_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11494881_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Sen","year":"2005","unstructured":"Sen, K., Ro\u015fu, G., Agha, G.: Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol.\u00a03535, Springer, Heidelberg (2005)"},{"key":"40_CR53","unstructured":"Specware. http:\/\/www.specware.org"},{"key":"40_CR54","unstructured":"SPIN. http:\/\/spinroot.com"},{"key":"40_CR55","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Fifth Workshop on Runtime Verification (RV 2005)","author":"V. Stolz","year":"2005","unstructured":"Stolz, V., Bodden, E.: Temporal Assertions using AspectJ. In: Fifth Workshop on Runtime Verification (RV 2005). Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, Amsterdam (2005)"},{"key":"40_CR56","unstructured":"T-UPPAAL. http:\/\/www.cs.aau.dk\/~marius\/tuppaal"},{"key":"40_CR57","unstructured":"Thati, P., Rosu, G.: Monitoring Algorithms for Metric Temporal Logic Specifications. In: Proceedings of the 4th International Workshop on Runtime Verification (RV 2004)[1], pp. 131\u2013147 (2004)"},{"key":"40_CR58","unstructured":"Valgrind. http:\/\/valgrind.org"},{"key":"40_CR59","doi-asserted-by":"crossref","unstructured":"Vanderperren, W., Suv\u00e9, D., Augustina Cibr\u00e1n, M., De Fraine, B.: Stateful Aspects in JAsCo. In: Workshop on Software Composition, ETAPS 2005 (2005)","DOI":"10.1007\/11550679_13"},{"key":"40_CR60","unstructured":"VDM. http:\/\/www.csr.ncl.ac.uk\/vdm"},{"key":"40_CR61","volume-title":"Proceedings 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: Proceedings of ASE 2000: The 15th IEEE International Conference on Automated Software Engineering, September 2000, IEEE CS Press, Los Alamitos (2000)"},{"key":"40_CR62","volume-title":"12th International Symposium on the Foundations of Software Engineering","author":"R.J. Walker","year":"2004","unstructured":"Walker, R.J., Viggers, K.: Implementing Protocols via Declarative Event Patterns. In: Taylor, R.N., Dwyer, M.B. (eds.) 12th International Symposium on the Foundations of Software Engineering, ACM, New York (2004)"},{"key":"40_CR63","doi-asserted-by":"crossref","unstructured":"Wang, L., Stoller, S.: Run-Time Analysis for Atomicity. In: Proceedings of the 3rd International Workshop on Runtime Verification (RV 2003) [1] (2003)","DOI":"10.1016\/S1571-0661(04)81049-1"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T12:00:01Z","timestamp":1738324801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}