{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:28:05Z","timestamp":1768908485947,"version":"3.49.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,4,21]],"date-time":"2011-04-21T00:00:00Z","timestamp":1303344000000},"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-0196-8","type":"journal-article","created":{"date-parts":[[2011,4,20]],"date-time":"2011-04-20T01:45:17Z","timestamp":1303263917000},"page":"349-382","source":"Crossref","is-referenced-by-count":118,"title":["What can you verify and enforce at runtime?"],"prefix":"10.1007","volume":"14","author":[{"given":"Yli\u00e8s","family":"Falcone","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Claude","family":"Fernandez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Mounier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,4,21]]},"reference":[{"issue":"4","key":"196_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern B., Schneider F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"196_CR2","doi-asserted-by":"crossref","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. 20(3), 675\u2013706 (2010)","journal-title":"J. Log. Comput."},{"key":"196_CR3","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. Technical Report TUM-I0724, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, December 2007"},{"issue":"3","key":"196_CR4","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":"196_CR5","doi-asserted-by":"crossref","unstructured":"Chang, E., Manna, Z., Pnueli, A.: The Safety-Progress Classification. Technical report, Department of Computer Science, Stanford University (1992)","DOI":"10.1007\/978-3-642-58041-3_5"},{"key":"196_CR6","doi-asserted-by":"crossref","unstructured":"Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Automata, Languages and Programming, pp. 474\u2013486 (1992)","DOI":"10.1007\/3-540-55719-9_97"},{"key":"196_CR7","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\u201907), pp. 569\u2013588. ACM press, New York (2007)","DOI":"10.1145\/1297027.1297069"},{"key":"196_CR8","first-page":"246","volume-title":"TACAS, Lecture Notes in Computer Science, vol. 5505","author":"F. Chen","year":"2009","unstructured":"Chen F., Ro\u015fu G.: Parametric trace slicing and monitoring. In: Kowalewski, S., Philippou, A. (eds) TACAS, Lecture Notes in Computer Science, vol. 5505, pp. 246\u2013261. Springer, Berlin (2009)"},{"key":"196_CR9","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"Clarke E.M., Wing J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28, 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"issue":"2\u20133","key":"196_CR10","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot P., Cousot R.: Abstract interpretation and application to logic programs. J. Log. Program. 13(2\u20133), 103\u2013179 (1992)","journal-title":"J. Log. Program."},{"key":"196_CR11","doi-asserted-by":"crossref","unstructured":"d\u2019Amorim, M., Ro\u015fu, G.: Efficient monitoring of \u03c9-languages. In: Proceedings of 17th International Conference on Computer-aided Verification (CAV\u201905). Lecture Notes in Computer Science, vol. 3576, pp. 364\u2013378. Springer, Berlin (2005)","DOI":"10.1007\/11513988_36"},{"key":"196_CR12","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Proceedings of the 7th Colloquium on Automata, Languages and Programming, pp. 169\u2013181. Springer, Berlin (1980)","DOI":"10.1007\/3-540-10003-2_69"},{"key":"196_CR13","first-page":"89","volume-title":"RV. Lecture Notes in Computer Science, vol. 6418","author":"Y. Falcone","year":"2010","unstructured":"Falcone Y.: You should better enforce than verify. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds) RV. Lecture Notes in Computer Science, vol. 6418, pp. 89\u2013105. Springer, Berlin (2010)"},{"key":"196_CR14","first-page":"30","volume-title":"ICTSS. Lecture Notes in Computer Science, vol. 6435","author":"Y. Falcone","year":"2010","unstructured":"Falcone Y., Fernandez J.-C., J\u00e9ron T., Marchand H., Mounier L.: More testable properties. In: Petrenko, A., daSilva Sim\u00e3o, A., Maldonado, J.C. (eds) ICTSS. Lecture Notes in Computer Science, vol. 6435, pp. 30\u201346. Springer, Berlin (2010)"},{"key":"196_CR15","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: Synthesizing enforcement monitors wrt. the Safety-Progress classification of properties. In: ICISS \u201908: Proceedings of the 4th International Conference on Information Systems Security, pp. 41\u201355. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-89862-7_3"},{"key":"196_CR16","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: Enforcement monitoring wrt. the Safety-Progress classification of properties. In: SAC \u201909: Proceedings of the 2009 ACM symposium on Applied Computing, pp. 593\u2013600. ACM Press, New York (2009)","DOI":"10.1145\/1529282.1529408"},{"key":"196_CR17","first-page":"40","volume-title":"RV. Lecture Notes in Computer Science, vol. 5779","author":"Y. Falcone","year":"2009","unstructured":"Falcone Y., Fernandez J.-C., Mounier L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D. (eds) RV. Lecture Notes in Computer Science, vol. 5779, pp. 40\u201359. Springer, Belin (2009)"},{"key":"196_CR18","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3) (2011)","DOI":"10.1007\/s10703-011-0114-4"},{"key":"196_CR19","doi-asserted-by":"crossref","unstructured":"Fong, P.W.L.: Access control by tracking shallow execution history. In: Proceedings of the 2004 IEEE Symposium on Security and Privacy, pp. 43\u201355. IEEE Computer Society Press, Los Alamitos (2004)","DOI":"10.1109\/SECPRI.2004.1301314"},{"issue":"1","key":"196_CR20","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/1111596.1111601","volume":"28","author":"K.W. Hamlen","year":"2006","unstructured":"Hamlen K.W., Morrisett G., Schneider F.B.: Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst. 28(1), 175\u2013205 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"196_CR21","doi-asserted-by":"crossref","unstructured":"Havelund, K., Goldberg, A.: Verify your runs. In: Verified Software: Theories, Tools, Experiments: First IFIP TC 2\/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, 10\u201313 Oct 2005, Revised Selected Papers and Discussions, pp. 374\u2013383. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-69149-5_40"},{"key":"196_CR22","unstructured":"Havelund, K., Ro\u015fu, G.: Efficient monitoring of safety properties. Softw. Tools Technol. Transf. 6(2), 158\u2013173 (2002)"},{"key":"196_CR23","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft J.E., Ullman J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, MA (1979)"},{"issue":"3","key":"196_CR24","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman O., Vardi M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"196_CR25","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"5","key":"196_CR26","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M. Leucker","year":"2008","unstructured":"Leucker M., Schallhart C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293\u2013303 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"196_CR27","doi-asserted-by":"crossref","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Enforcing non-safety security policies with program monitors. In: ESORICS, pp. 355\u2013373 (2005)","DOI":"10.1007\/11555827_21"},{"issue":"3","key":"196_CR28","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. Inf. Syst. Secur. 12(3), 1\u201341 (2009)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"196_CR29","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties (invited paper, 1989). In: PODC \u201990: Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing, pp. 377\u2013410. ACM Press, New York (1990)","DOI":"10.1145\/93385.93442"},{"key":"196_CR30","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.entcs.2006.08.029","volume":"179","author":"F. Martinelli","year":"2007","unstructured":"Martinelli F., Matteucci I.: Through modeling to synthesis of security automata. Electron. Notes Theor. Comput. Sci. 179, 31\u201346 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"196_CR31","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.entcs.2007.03.025","volume":"186","author":"I. Matteucci","year":"2007","unstructured":"Matteucci I.: Automated synthesis of enforcing mechanisms for security properties in a timed setting. Electron. Notes Theor. Comput. Sci. 186, 101\u2013120 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"196_CR32","first-page":"573","volume-title":"FM. Lecture Notes in Computer Science, vol. 4085","author":"A. Pnueli","year":"2006","unstructured":"Pnueli A., Zaks A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM. Lecture Notes in Computer Science, vol. 4085, pp. 573\u2013586. Springer, Berlin (2006)"},{"key":"196_CR33","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., Chen, F., Ball, T.: Synthesizing monitors for safety properties\u2014this time with calls and returns. In: Workshop on Runtime Verification (RV\u201908). Lecture Notes in Computer Science, vol. 5289, pp. 51\u201368. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-89247-2_4"},{"key":"196_CR34","unstructured":"Runtime Verification, 2001\u20132010. http:\/\/www.runtime-verification.org"},{"issue":"1","key":"196_CR35","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. Inf. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"196_CR36","doi-asserted-by":"crossref","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse. In: STOC \u201981: Proceedings of the 13th Annual ACM Symposium on Theory of Computing, pp. 375\u2013383. ACM Press, New York (1981)","DOI":"10.1145\/800076.802492"},{"key":"196_CR37","first-page":"543","volume-title":"ICTAC. Lecture Notes in Computer Science, vol. 3407","author":"M. Viswanathan","year":"2004","unstructured":"Viswanathan M., Kim M.: Foundations for the run-time monitoring of reactive systems\u2014fundamentals of the MaC language. In: Liu, Z., Araki, K. (eds) ICTAC. Lecture Notes in Computer Science, vol. 3407, pp. 543\u2013556. Springer, Berlin (2004)"}],"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-0196-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0196-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0196-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T04:44:58Z","timestamp":1741149898000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0196-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,4,21]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["196"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0196-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,4,21]]}}}