{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:17:18Z","timestamp":1759033038415},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,11,29]],"date-time":"2011-11-29T00:00:00Z","timestamp":1322524800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,6]]},"DOI":"10.1007\/s10009-011-0218-6","type":"journal-article","created":{"date-parts":[[2011,11,28]],"date-time":"2011-11-28T10:22:55Z","timestamp":1322475775000},"page":"243-247","source":"Crossref","is-referenced-by-count":18,"title":["Introduction to the special section on runtime verification"],"prefix":"10.1007","volume":"14","author":[{"given":"Oleg","family":"Sokolsky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,11,29]]},"reference":[{"key":"218_CR1","doi-asserted-by":"crossref","unstructured":"Allan, C., Avgustinov, P., Kuzins, S., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J., Christensen, A.S., Hendren, L., Lhot\u00e1k, O.: Adding trace matching with free variables to AspectJ. In: Proceedings of the 20th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA\u201905), pp. 345\u2013364, October 2005","DOI":"10.1145\/1094811.1094839"},{"key":"218_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS\u201904). LNCS, vol. 3362, March 2004","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"218_CR3","doi-asserted-by":"crossref","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Proceedings of 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI\u201904). LNCS, vol. 2937, pp. 44\u201357, January 2004","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"218_CR4","doi-asserted-by":"crossref","unstructured":"Barringer, H., Havelund, K.: TraceContract: a Scala DSL for trace analysis. In: Proceedings of 17th International Symposium on Formal Methods(FM\u201911). LNCS, vol. 6664, June 2011","DOI":"10.1007\/978-3-642-21437-0_7"},{"key":"218_CR5","doi-asserted-by":"crossref","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: From Eagle to RuleR. In: Proceedings of the 7th Workshop on Runtime Verification (RV\u201907). LNCS, vol. 4839, pp. 111\u2013125, March 2007","DOI":"10.1007\/978-3-540-77395-5_10"},{"key":"218_CR6","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass\u2014Java with assertions. In: Proceedings of the 1st Workshop on Runtime Verification (RV\u201901), July 2001"},{"key":"218_CR7","doi-asserted-by":"crossref","unstructured":"Bartussek, W., Parnas, D.L.: Using assertions about traces to write abstract specifications for software modules. In: Proceedings of the 2nd Conference on European Cooperation in Informatics. LNCS, vol. 65, pp. 211\u2013236 (1978)","DOI":"10.1007\/3-540-08934-9_80"},{"key":"218_CR8","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Model-based runtime analysis of distributed reactive systems. In: Proceedings of the 2006 Australian Software Engineering Conference (ASWEC\u201906), pp. 243\u2013252, April 2006","DOI":"10.1109\/ASWEC.2006.36"},{"issue":"3","key":"218_CR9","doi-asserted-by":"crossref","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. J. Log. Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Log. Comput."},{"key":"218_CR10","doi-asserted-by":"crossref","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. In: Proceedings of the 21st Annual ACM Symposium on Theory of Computing, pp. 86\u201397, May 1989","DOI":"10.1145\/73007.73015"},{"key":"218_CR11","doi-asserted-by":"crossref","unstructured":"Bodden, E.: A lightweight LTL runtime verification tool for Java. In: 9th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA\u201904), pp. 306\u2013307, October 2004","DOI":"10.1145\/1028664.1028776"},{"key":"218_CR12","doi-asserted-by":"crossref","unstructured":"Bodden, E.: Efficient hybrid typestate analysis by determining continuation-equivalent states. In: International Conference on Software Engineering (ICSE\u201910), pp. 5\u201314, May 2010","DOI":"10.1145\/1806799.1806805"},{"key":"218_CR13","doi-asserted-by":"crossref","unstructured":"Bodden E., Hendren, L.: The Clara framework for hybrid typestate analysis. Software Tools for Technology Transfer, Special Section on Runtime Verification, in this volume (2011)","DOI":"10.1007\/s10009-010-0183-5"},{"key":"218_CR14","doi-asserted-by":"crossref","unstructured":"Bodden, E., Hendren, L., Lhot\u00e1k, O.: A staged static program analysis to improve the performance of runtime monitoring. In: Proceedings of the 21st European Conference on Object-Oriented Programming (ECOOP\u201907). LNCS, vol. 4609, pp. 525\u2013549, July 2007","DOI":"10.1007\/978-3-540-73589-2_25"},{"issue":"3","key":"218_CR15","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy L., Cheon Y., Cok D., Ernst M., Kiniry J., Leavens G.T., Leino K.R.M., Poll E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"218_CR16","doi-asserted-by":"crossref","unstructured":"Chen, K., Malik, S., Patra, P.: Runtime validation of transactional memory systems. In: International Symposium on Quality Electronic Design, pp. 750\u2013756 (2008)","DOI":"10.1109\/ISQED.2008.4479832"},{"key":"218_CR17","volume-title":"Model checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke E.M., Grumberg O., Peled D.A.: Model checking. MIT Press, Cambridge (2000)"},{"key":"218_CR18","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G., Abela, P.: Compensation-aware runtime monitoring. In: Proceedings of the 1st International Conference on Runtime Verificaiton (RV\u201910). LNCS, vol. 6418, pp. 214\u2013228, November 2010","DOI":"10.1007\/978-3-642-16612-9_17"},{"key":"218_CR19","doi-asserted-by":"crossref","unstructured":"D\u2019Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. In: Workshop on Dynamic Program Analysis (WODA\u201905). ACM Sigsoft Software Engineering Notes, vol. 30, pp. 1\u20137 (2005)","DOI":"10.1145\/1082983.1083249"},{"key":"218_CR20","unstructured":"De Pauw, W., Heisig, S.: Visual and algorithmic tooling for system trace analysis: a case study. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP\u201909), 2009"},{"key":"218_CR21","unstructured":"Drusinsky, D.: The Temporal Rover and the ATG Rover. In: SPIN Model Checking and Software Verification. LNCS, vol. 1885, pp. 323\u2013330 (2000)"},{"key":"218_CR22","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Purandare, R.: Residual dynamic typestate analysis: Exploiting static analysis results to reformulate and reduce the cost of dynamic analysis. In: Proceedings of the 22nd International Conference on Automated Software Engineering (ASE\u201907), pp. 124\u2013133, November 2007","DOI":"10.1145\/1321631.1321651"},{"key":"218_CR23","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: Efficiently computing the happens-before relation using locksets. In: Proceedings of the Workshop on Formal Approaches to Testing and Runtime Verification (FATES\/RV\u201906), August 2006","DOI":"10.1007\/11940197_13"},{"key":"218_CR24","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: Proceedings of the 2010 ACM Symposium on Applied Computing (SAC\u201910), pp. 2103\u20132110 (2010)","DOI":"10.1145\/1774088.1774531"},{"key":"218_CR25","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? Software Tools for Technology Transfer, Special Section on Runtime Verification, in this volume (2011)","DOI":"10.1007\/s10009-011-0196-8"},{"issue":"3","key":"218_CR26","doi-asserted-by":"crossref","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 about runtime executions. Formal Methods Syst. Des. 27(3), 253\u2013274 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"218_CR27","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Monitoring Java programs with JavaPathExplorer. In: Proceedings of the 1st Workshop on Runtime Verification. Electronic Notes in Theoretical Computer Science, vol. 55, Elsevier Publishing (2001)","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"218_CR28","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201902), volume 2280 of LNCS, pages 342\u2013356, (April 2002)","DOI":"10.1007\/3-540-46002-0_24"},{"issue":"2","key":"218_CR29","doi-asserted-by":"crossref","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. Int. J. Softw. Tools Technol. Transf. 6(2), 158\u2013173 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"218_CR30","doi-asserted-by":"crossref","unstructured":"Huang, X., Seyster, J., Callanan, S., Dixit, K., Grosu, R., Smolka, S.A., Stoller, S.D., Zadok, E.: Software monitoring with controllable overhead. Software Tools for Technology Transfer, Special Section on Runtime Verification, in this volume (2011)","DOI":"10.1007\/s10009-010-0184-4"},{"key":"218_CR31","doi-asserted-by":"crossref","unstructured":"Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Videira Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Proceedings of the European Conference on Object-Oriented Programming (ECOOP). LNCS, vol. 1241, pp. 220\u2013242, June 1997","DOI":"10.1007\/BFb0053381"},{"issue":"2","key":"218_CR32","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M. Kim","year":"2004","unstructured":"Kim M., Kannan S., Lee I., Sokolsky O., Viswanathan M.: Java-MaC: a run-time assurance approach for Java programs. Formal Methods Syst. Des. 24(2), 129\u2013155 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"218_CR33","unstructured":"Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA\u201999), June 1999"},{"issue":"3","key":"218_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1455526.1455532","volume":"12","author":"J. Ligatti","year":"2009","unstructured":"Ligatti J., Bauer L., Walker D.: Run-time enforcement of nonsafety policies. ACM Trans. Inform. Syst. Secur. 12(3), 1\u201341 (2009)","journal-title":"ACM Trans. Inform. Syst. Secur."},{"key":"218_CR35","doi-asserted-by":"crossref","unstructured":"Meredith, P., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. Software Tools for Technology Transfer, Special Section on Runtime Verification, in this volume (2011)","DOI":"10.1007\/s10009-011-0198-6"},{"key":"218_CR36","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer B.: Object-Oriented Software Construction. Prentice Hall, Englewood Cliffs (1988)"},{"key":"218_CR37","doi-asserted-by":"crossref","unstructured":"Pellizzoni, R., Meredith, P., Caccamo, M., Rosu, G.: Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In: Proceedings of the 29th Real-Time Systems Symposium (RTSS\u201909), pp. 481\u2013491, December 2008","DOI":"10.1109\/RTSS.2008.43"},{"key":"218_CR38","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Tasiran, S.: Runtime verification of concurrency-specific correctness criteria. Software Tools for Technology Transfer, Special Section on Runtime Verification, in this volume (2011)","DOI":"10.1007\/s10009-011-0210-1"},{"key":"218_CR39","doi-asserted-by":"crossref","unstructured":"Sammapun, U., Lee, I., Sokolsky, O., Regehr, J.: Statistical runtime checking of probabilistic properties. In: Proceedings of the 7th Workshop on Runtime Verification. LNCS, vol. 4839, pp. 164\u2013175, March 2007","DOI":"10.1007\/978-3-540-77395-5_14"},{"issue":"1","key":"218_CR40","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F.B. Schneider","year":"2000","unstructured":"Schneider F.B.: Enforceable security policies. ACM Trans. Inform. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inform. Syst. Secur."},{"key":"218_CR41","doi-asserted-by":"crossref","unstructured":"Seyster, J., Dixit, K., Huang, X., Grosu, R., Havelund, K., Smolka, S.A., Stoller, S.D., Zadok, E.: Aspect-oriented instrumentation with GCC. In: Proceedings of the 1st International Conference on Runtime Verification. LNCS, vol. 6418, pp. 405\u2013420, November 2010","DOI":"10.1007\/978-3-642-16612-9_31"},{"key":"218_CR42","doi-asserted-by":"crossref","unstructured":"Tripakis, S.: A combined on-line\/off-line framework for black-box fault diagnosis. In: Proceedings of the 9th Workshop on Runtime Verification (RV\u201909), pp. 152\u2013167, July 2009","DOI":"10.1007\/978-3-642-04694-0_11"},{"key":"218_CR43","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L. Wang","year":"2006","unstructured":"Wang L., Stoller S.D.: Runtime analysis of atomicity for multi-threaded programs. IEEE Trans. Softw. Eng. 32, 93\u2013110 (2006)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0218-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0218-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0218-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,20]],"date-time":"2019-06-20T03:02:50Z","timestamp":1560999770000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0218-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,29]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["218"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0218-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11,29]]}}}