{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T08:59:05Z","timestamp":1766048345175,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642298592"},{"type":"electronic","value":"9783642298608"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29860-8_4","type":"book-chapter","created":{"date-parts":[[2012,5,11]],"date-time":"2012-05-11T13:38:03Z","timestamp":1336743483000},"page":"34-48","source":"Crossref","is-referenced-by-count":20,"title":["Teaching Runtime Verification"],"prefix":"10.1007","author":[{"given":"Martin","family":"Leucker","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"12","key":"4_CR1","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1109\/TSE.2004.91","volume":"30","author":"N. Delgado","year":"2004","unstructured":"Delgado, N., Gates, A.Q., Roach, S.: A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Transactions on Software Engineering (TSE)\u00a030(12), 859\u2013872 (2004)","journal-title":"IEEE Transactions on Software Engineering (TSE)"},{"key":"4_CR2","unstructured":"IEEE Std 1012 - 2004 IEEE standard for software verificiation and validation. IEEE Std 1012-2004 (Revision of IEEE Std 1012-1998), 1\u2013110 (2005)"},{"key":"4_CR3","series-title":"An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"4_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"4_CR5","unstructured":"Myers, G.J., Badgett, T., Thomas, T.M., Sandler, C.: The Art of Software Testing, 2nd edn. John Wiley and Sons (2004)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/11498490_18","volume-title":"Model-Based Testing of Reactive Systems","year":"2005","unstructured":"Broy, M., Jonsson, B., Katoen, J.P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol.\u00a03472, pp. 391\u2013438. Springer, Heidelberg (2005)"},{"key":"4_CR7","first-page":"46","volume-title":"Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS-77)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS-77), October 31-November 2, pp. 46\u201357. IEEE Computer Society Press, Providence (1977)"},{"key":"4_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"4_CR9","unstructured":"Kamp, H.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles (1968)"},{"key":"4_CR10","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":"4_CR11","doi-asserted-by":"crossref","unstructured":"Geilen, M.: On the construction of monitors for temporal logic properties. Electronic Notes on Theoretical Computer Science (ENTCS) 55(2) (2001)","DOI":"10.1016\/S1571-0661(04)00252-X"},{"key":"4_CR12","first-page":"332","volume-title":"Symposium on Logic in Computer Science (LICS 1986)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science (LICS 1986), pp. 332\u2013345. IEEE Computer Society Press, Washington, D.C (1986)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An Automata-Theoretic Approach to Linear Temporal Logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11944836_25","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Monitoring of Real-Time Properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol.\u00a04337, pp. 260\u2013272. Springer, Heidelberg (2006)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) 20(4) (July 2011) (in press)","DOI":"10.1145\/2000799.2000800"},{"issue":"3","key":"4_CR16","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A. Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. Journal of Logic and Computation\u00a020(3), 651\u2013674 (2010)","journal-title":"Journal of Logic and Computation"},{"key":"4_CR17","unstructured":"Hochberger, C., Leucker, M., Weiss, A., Backasch, R.: A generic hardware architecture for runtime verification. In: ECSI (ed.) Proceedings of the 2010 Conference on System, Software, SoC and Silicon Debug, pp. 79\u201384 (2010)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Model-based runtime analysis of distributed reactive systems. In: Proceedings of the Australian Software Engineering Conference (ASWEC 2006), pp. 243\u2013252. IEEE (2006)","DOI":"10.1109\/ASWEC.2006.36"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","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, pp. 44\u201357. Springer, Heidelberg (2004)"},{"key":"4_CR20","unstructured":"Stolz, V., Bodden, E.: Temporal Assertions using AspectJ. In: Fifth Workshop on Runtime Verification (RV 2005). ENTCS, Elsevier (2005)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Larva \u2014 safer monitoring of real-time java programs (tool paper). In: Hung, D.V., Krishnan, P. (eds.) SEFM, pp. 33\u201337. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.13"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.H.: An entry point for formal methods: Specification and analysis of event logs. In: Bujorianu, M.L., Fisher, M. (eds.) FMA. EPTCS, vol.\u00a020, pp. 16\u201321 (2009)","DOI":"10.4204\/EPTCS.20.2"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166\u2013174 (2005)","DOI":"10.1109\/TIME.2005.26"},{"issue":"2","key":"4_CR24","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M. Kim","year":"2004","unstructured":"Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-mac: A run-time assurance approach for java programs. Formal Methods in System Design\u00a024(2), 129\u2013155 (2004)","journal-title":"Formal Methods in System Design"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Chen, F., Ro\u015fu, G.: MOP: An Efficient and Generic Runtime Verification Framework. In: Object-Oriented Programming, Systems, Languages and Applications, OOPSLA 2007 (2007)","DOI":"10.1145\/1297027.1297069"},{"issue":"3","key":"4_CR26","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H. Barringer","year":"2010","unstructured":"Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from eagle to ruler. J. Log. Comput.\u00a020(3), 675\u2013706 (2010)","journal-title":"J. Log. Comput."},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-21437-0_7","volume-title":"FM 2011: Formal Methods","author":"H. Barringer","year":"2011","unstructured":"Barringer, H., Havelund, K.: TraceContract: A Scala DSL for Trace Analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 57\u201372. Springer, Heidelberg (2011)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Avgustinov, P., Tibble, J., Bodden, E., Hendren, L.J., Lhot\u00e1k, O., de Moor, O., Ongkingco, N., Sittampalam, G.: Efficient trace monitoring. In: Tarr, P.L., Cook, W.R. (eds.) OOPSLA Companion, pp. 685\u2013686. ACM (2006)","DOI":"10.1145\/1176617.1176673"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29860-8_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:46:46Z","timestamp":1743108406000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29860-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642298592","9783642298608"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29860-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}