{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:07:55Z","timestamp":1743116875280,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319469812"},{"type":"electronic","value":"9783319469829"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46982-9_5","type":"book-chapter","created":{"date-parts":[[2016,9,19]],"date-time":"2016-09-19T11:41:08Z","timestamp":1474285268000},"page":"46-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Runtime Verification at Work: A Tutorial"],"prefix":"10.1007","author":[{"given":"Philip","family":"Daian","sequence":"first","affiliation":[]},{"given":"Dwight","family":"Guth","sequence":"additional","affiliation":[]},{"given":"Chris","family":"Hathhorn","sequence":"additional","affiliation":[]},{"given":"Yilong","family":"Li","sequence":"additional","affiliation":[]},{"given":"Edgar","family":"Pek","sequence":"additional","affiliation":[]},{"given":"Manasvi","family":"Saxena","sequence":"additional","affiliation":[]},{"given":"Traian Florin","family":"\u015eerb\u0103nu\u0163\u0103","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,20]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. In: 79.6, pp. 397\u2013434 (2010). doi:\n                      10.1016\/j.jlap.03.012","DOI":"10.1016\/j.jlap.03.012"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-35632-2_16","volume-title":"Runtime Verification","author":"TF \u015eerb\u0103nu\u0163\u0103","year":"2013","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Chen, F., Ro\u015fu, G.: Maximal causal models for sequentially consistent systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 136\u2013150. Springer, Heidelberg (2013). doi:\n                      10.1007\/978-3-642-35632-2_16"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1007\/978-3-662-49674-9_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2016","unstructured":"Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (Report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887\u2013904. Springer, Heidelberg (2016). doi:\n                      10.1007\/978-3-662-49674-9_55"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-35308-6_8","volume-title":"Certified Programs and Proofs","author":"B Campbell","year":"2012","unstructured":"Campbell, B.: An executable semantics for CompCert C. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 60\u201375. Springer, Heidelberg (2012). doi:\n                      10.1007\/978-3-642-35308-6_8"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Canet, G., Cuoq, P., Monate, B.: A value analysis for C programs. In: Conference on Source Code Analysis and Manipulation (SCAM 2009), pp. 123\u2013124. IEEE (2009). doi:\n                      10.1109\/SCAM.2009.22","DOI":"10.1109\/SCAM.2009.22"},{"key":"5_CR6","unstructured":"Clang: Clang 3.9 Documentation. \n                      http:\/\/clang.llvm.org\/docs\/index.html"},{"key":"5_CR7","unstructured":"Daian, P.: RV-Monitor Documentation (2015). \n                      https:\/\/runtimeverification.com\/monitor\/1.3\/docs\/"},{"key":"5_CR8","unstructured":"Ellison, C.: A formal semantics of C with applications. Ph.D. thesis. University of Illinois, July 2012. \n                      http:\/\/hdl.handle.net\/2142\/34297"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pp. 533\u2013544 (2012). doi:\n                      10.1145\/2103656.2103719.","DOI":"10.1145\/2103656.2103719."},{"key":"5_CR10","unstructured":"GrammaTech: CodeSonar. \n                      http:\/\/grammatech.com\/products\/codesonar"},{"key":"5_CR11","unstructured":"Guth, D.: RV-Match Documentation (2016). \n                      https:\/\/runtimeverification.com\/match\/1.0-SNAPSHOT\/docs\/"},{"key":"5_CR12","unstructured":"Guth, D.: Using RV-Predict to track down race conditions (2015). \n                      https:\/\/runtimeverification.com\/blog\/?p=47"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Hathhorn, C., Ellison, C., Ro\u015fu, G.: Defining the undefinedness of C. In: 36th Conference on Programming Language Design and Implementation (PLDI 2015) (2015)","DOI":"10.1145\/2737924.2737979"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Huang, J., Meredith, Patrick O\u2019Neil Ro\u015fu, G.: Maximal sound predictive race detection with control flow abstraction. In: PLDI 2015. doi:\n                      10.1145\/2594291.2594315","DOI":"10.1145\/2594291.2594315"},{"key":"5_CR15","unstructured":"ISO, IEC JTC 1, SC 22, WG 14. ISO, IEC 9899: 2011: Prog. Lang.\u2013C. Tech. rep. International Organization for Standardization, 2012"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Jin, D., et al.: JavaMOP: efficient parametric runtime monitoring framework. In: ICSE 2012, pp. 1427\u20131430. IEEE, June 2012. \n                      http:\/\/dx.doi.org\/10.1109\/ICSE.2012.6227231","DOI":"10.1109\/ICSE.2012.6227231"},{"key":"5_CR17","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 \u2014 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. 2072, pp. 327\u2013354. Springer, Heidelberg (2001). doi:\n                      10.1007\/3-540-45337-7_18"},{"key":"5_CR18","unstructured":"Li, Y.: Detecting popular data races in Java using RV-Predict (2015). \n                      https:\/\/runtimeverification.com\/blog\/?p=58"},{"key":"5_CR19","unstructured":"Li, Y.: RV-Predict Documentation (2015). \n                      https:\/\/runtimeverification.com\/predict\/1.8.2\/docs\/"},{"key":"5_CR20","series-title":"The SEI Series in Software Engineering","volume-title":"The CERT Oracle Secure Coding Standard for Java","author":"F Long","year":"2012","unstructured":"Long, F., et al.: The CERT Oracle Secure Coding Standard for Java. The SEI Series in Software Engineering. Addison-Wesley, Upper Saddle River (2012). ISBN: 978-0-321-80395-5"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-11164-3_24","volume-title":"Runtime Verification","author":"Q Luo","year":"2014","unstructured":"Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: RV-Monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 285\u2013300. Springer, Heidelberg (2014). doi:\n                      10.1007\/978-3-319-11164-3_24"},{"key":"5_CR22","unstructured":"MathWorks. Polyspace Bug Finder. \n                      http:\/\/www.mathworks.com\/products\/polyspace-bug-finder"},{"key":"5_CR23","unstructured":"MathWorks. Polyspace Code Prover. \n                      http:\/\/www.mathworks.com\/products\/polyspace-code-prover"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2007), pp. 89\u2013100. ACM (2007). doi:\n                      10.1145\/1250734.1250746","DOI":"10.1145\/1250734.1250746"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Shiraishi, S., Mohan, V., Marimuthu, H.: Test suites for benchmarks of static analysis tools. In: The 26th IEEE International Symposium on Software Reliability Engineering (ISSRE 2015), vol. Industrial Track (2015)","DOI":"10.1109\/ISSREW.2015.7392027"},{"key":"5_CR26","unstructured":"Why does this Java program terminate despite that apparently it shouldn\u2019t (and didn\u2019t)? (2013) \n                      http:\/\/stackoverflow.com\/questions\/16159203\/whydoes-this-java-program-terminate-despite-that-apparently-itshouldnt-and-d"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46982-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:28:14Z","timestamp":1558315694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46982-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319469812","9783319469829"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46982-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"20 September 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}