{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:24:13Z","timestamp":1777519453608,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642214363","type":"print"},{"value":"9783642214370","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_7","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T03:33:16Z","timestamp":1308367996000},"page":"57-72","source":"Crossref","is-referenced-by-count":78,"title":["TraceContract: A Scala DSL for Trace Analysis"],"prefix":"10.1007","author":[{"given":"Howard","family":"Barringer","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"NASA\u2019s LADEE (Lunar Atmosphere and Dust Environment Explorer) mission, http:\/\/www.nasa.gov\/mission_pages\/LADEE\/main"},{"key":"7_CR2","unstructured":"The Scala programming language, http:\/\/www.scala-lang.org"},{"key":"7_CR3","volume-title":"OOPSLA 2005","author":"C. Allan","year":"2005","unstructured":"Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhot\u00e1k, O., de Moor, O., Sereni, D., Sittamplan, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA 2005. ACM Press, New York (2005)"},{"key":"7_CR4","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)"},{"issue":"11","key":"7_CR5","doi-asserted-by":"publisher","first-page":"365","DOI":"10.2514\/1.49356","volume":"7","author":"H. Barringer","year":"2010","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.: Formal analysis of log files. Journal of Aerospace Computing, Information, and Communication\u00a07(11), 365\u2013390 (2010)","journal-title":"Journal of Aerospace Computing, Information, and Communication"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-04694-0_1","volume-title":"Runtime Verification","author":"H. Barringer","year":"2009","unstructured":"Barringer, H., Havelund, K., Rydeheard, D., Groce, A.: Rule systems for runtime verification: A short tutorial. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol.\u00a05779, pp. 1\u201324. Springer, Heidelberg (2009)"},{"issue":"3","key":"7_CR7","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":"7_CR8","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"},{"key":"7_CR9","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)"},{"issue":"3","key":"7_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10703-005-3399-3","volume":"27","author":"B. Finkbeiner","year":"2005","unstructured":"Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting statistics over runtime executions. Formal Methods in System Design\u00a027(3), 253\u2013274 (2005)","journal-title":"Formal Methods in System Design"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-74591-4_27","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2007","unstructured":"Garillot, F., Werner, B.: Simple types in type theory: Deep and shallow encodings. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 368\u2013382. Springer, Heidelberg (2007)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: 16th ASE conference, San Diego, CA, USA, pp. 135\u2013143 (2001)","DOI":"10.1109\/ASE.2001.989799"},{"key":"7_CR13","unstructured":"Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: PDPTA, pp. 279\u2013287. CSREA Press (1999)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-16612-9_5","volume-title":"Runtime Verification","author":"M. Odersky","year":"2010","unstructured":"Odersky, M.: Contracts for scala. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 51\u201357. Springer, Heidelberg (2010)"},{"key":"7_CR15","series-title":"ENTCS","first-page":"109","volume-title":"Proc. of the 5th Int. Workshop on Runtime Verification (RV 2005)","author":"V. Stolz","year":"2006","unstructured":"Stolz, V., Bodden, E.: Temporal assertions using AspectJ. In: Proc. of the 5th Int. Workshop on Runtime Verification (RV 2005). ENTCS, vol.\u00a0144(4), pp. 109\u2013124. Elsevier, Amsterdam (2006)"},{"key":"7_CR16","series-title":"ENTCS","first-page":"201","volume-title":"Proc. of the 4th Int. Workshop on Runtime Verification (RV 2004)","author":"V. Stolz","year":"2005","unstructured":"Stolz, V., Huch, F.: Runtime verification of concurrent Haskell programs. In: Proc. of the 4th Int. Workshop on Runtime Verification (RV 2004). ENTCS, vol.\u00a0113, pp. 201\u2013216. Elsevier, Amsterdam (2005)"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T20:07:10Z","timestamp":1560283630000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}