{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T05:04:40Z","timestamp":1768280680213,"version":"3.49.0"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319675305","type":"print"},{"value":"9783319675312","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-67531-2_14","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:33:37Z","timestamp":1504604017000},"page":"225-240","source":"Crossref","is-referenced-by-count":17,"title":["From Model Checking to Runtime Verification\u00a0and Back"],"prefix":"10.1007","author":[{"given":"Katar\u00edna","family":"Kejstov\u00e1","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J Barnat","year":"2013","unstructured":"Barnat, J., Brim, L., Havel, V., Havl\u00ed\u010dek, J., Kriho, J., Lenco, M., Ro\u010dkai, P., Still, V., Weiser, J.: DiVinE 3.0 \u2013 an explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-39799-8_60"},{"key":"14_CR2","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. 1885, pp. 245\u2013264. Springer, Heidelberg (2000). doi:\n10.1007\/10722468_15"},{"issue":"2","key":"14_CR3","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Rosu, G.: Efficient monitoring of safety properties. STTT 6(2), 158\u2013173 (2004). doi:\n10.1007\/s10009-003-0117-6","journal-title":"STTT"},{"issue":"2","key":"14_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/B:FORM.0000017721.39909.4b","volume":"24","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Rosu, G.: An overview of the runtime verification tool Java PathExplorer. Formal Methods Syst. Des. 24(2), 189\u2013215 (2004). doi:\n10.1023\/B:FORM.0000017721.39909.4b","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Jin, D., O\u2019Neil Meredith, P., Lee, C., Ro\u015fu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: International Conference on Software Engineering (ICSE), pp. 1427\u20131430. IEEE, June 2012. doi:\n10.1109\/ICSE.2012.6227231","DOI":"10.1109\/ICSE.2012.6227231"},{"issue":"2","key":"14_CR6","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 Syst. Des. 24(2), 129\u2013155 (2004). doi:\n10.1023\/B:FORM.0000017719.43755.7c\n\n. ISSN:1572\u20138102","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"14_CR7","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"P O\u2019Neil Meredith","year":"2012","unstructured":"O\u2019Neil Meredith, P., Jin, D., Griffith, D., Chen, F., Ro\u015fu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transfer 14(3), 249\u2013289 (2012). doi:\n10.1007\/s10009-011-0198-6\n\n. ISSN:1433\u20132787","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI (2007)","DOI":"10.1145\/1250734.1250746"},{"key":"14_CR9","unstructured":"The LLVM Project. LLVM language reference manual (2016). \nhttp:\/\/llvm.org\/docs\/LangRef.html"},{"key":"14_CR10","unstructured":"Petr Ro\u0109kai and Ji\u0159\u00ecBarnat. A simulator for LLVM bitcode. 2017. Preliminary version. \nhttps:\/\/arxiv.org\/abs\/1704.05551"},{"key":"14_CR11","unstructured":"Ro\u010dkai, P., \u0160till, V., \u010cern\u00e0, I., Barnat, J.: DiVM: model checking with LLVM and graph memory (2017). Preliminary version. \nhttps:\/\/arxiv.org\/abs\/1703.05341"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67531-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:37:15Z","timestamp":1504604235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67531-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675305","9783319675312"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67531-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}