{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T21:17:42Z","timestamp":1790716662136,"version":"4.1.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2012,6,1]],"date-time":"2012-06-01T00:00:00Z","timestamp":1338508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2012,6]]},"abstract":"<jats:p>Finite-state properties account for an important class of program properties, typically related to the order of operations invoked on objects. Many library implementations therefore include manually written finite-state monitors to detect violations of finite-state properties at runtime. Researchers have recently proposed the explicit specification of finite-state properties and automatic generation of monitors from the specification. However, runtime monitoring only shows the presence of violations, and typically cannot prove their absence. Moreover, inserting a runtime monitor into a program under test can slow down the program by several orders of magnitude.<\/jats:p>\n          <jats:p>In this work, we therefore present a set of four static whole-program analyses that partially evaluate runtime monitors at compile time, with increasing cost and precision. As we show, ahead-of-time evaluation can often evaluate the monitor completely statically. This may prove that the program cannot violate the property on any execution or may prove that violations do exist. In the remaining cases, the partial evaluation converts the runtime monitor into a residual monitor. This monitor only receives events from program locations that the analyses failed to prove irrelevant. This makes the residual monitor much more efficient than a full monitor, while still capturing all property violations at runtime.<\/jats:p>\n          <jats:p>We implemented the analyses in Clara, a novel framework for the partial evaluation of AspectJ-based runtime monitors, and validated our approach by applying Clara to finite-state properties over several large-scale Java programs. Clara proved that most of the programs never violate our example properties. Some programs required monitoring, but in those cases Clara could often reduce the monitoring overhead to below 10%. We observed that several programs did violate the stated properties.<\/jats:p>","DOI":"10.1145\/2220365.2220366","type":"journal-article","created":{"date-parts":[[2012,7,3]],"date-time":"2012-07-03T11:53:04Z","timestamp":1341316384000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Partially Evaluating Finite-State Runtime Monitors Ahead of Time"],"prefix":"10.1145","volume":"34","author":[{"given":"Eric","family":"Bodden","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Darmstadt"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrick","family":"Lam","sequence":"additional","affiliation":[{"name":"University of Waterloo"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurie","family":"Hendren","sequence":"additional","affiliation":[{"name":"McGill University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094839"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1052898.1052906"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Avgustinov P. Tibble J. Bodden E. Lhot\u00e1k O. Hendren L. de Moor O. Ongkingco N. and Sittampalam G. 2006. Efficient trace monitoring. Tech. rep. abc-2006-1. Avgustinov P. Tibble J. Bodden E. Lhot\u00e1k O. Hendren L. de Moor O. Ongkingco N. and Sittampalam G. 2006. Efficient trace monitoring. Tech. rep. abc-2006-1.","DOI":"10.1145\/1176617.1176673"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297070"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297050"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806805"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2394758.2394793"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453109"},{"key":"e_1_2_1_12_1","volume-title":"Visions of Computer Science: Proceedings of the BCS International Academic Conference. British Computing Society.","author":"Bodden E.","unstructured":"Bodden , E. , Lam , P. , and Hendren , L . 2008b. Object representatives: A uniform abstraction for pointer information . In Visions of Computer Science: Proceedings of the BCS International Academic Conference. British Computing Society. Bodden, E., Lam, P., and Hendren, L. 2008b. Object representatives: A uniform abstraction for pointer information. In Visions of Computer Science: Proceedings of the BCS International Academic Conference. British Computing Society."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1509239.1509243"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn077"},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science","volume-title":"Clara: A framework for statically evaluating finite-state runtime monitors. In Proceedings of the 1st International Conference on Runtime Verification","author":"Bodden E.","year":"2010","unstructured":"Bodden , E. , Lam , P. , and Hendren , L . 2010 b. Clara: A framework for statically evaluating finite-state runtime monitors. In Proceedings of the 1st International Conference on Runtime Verification . Lecture Notes in Computer Science , vol. 6418 , Springer , 74--88. Bodden, E., Lam, P., and Hendren, L. 2010b. Clara: A framework for statically evaluating finite-state runtime monitors. In Proceedings of the 1st International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 6418, Springer, 74--88."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985827"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the Symposium on Mathematical Theory of Automata. Polytechnic Institute of Brooklyn, 529--561","author":"Brzozowski J. A.","year":"1962","unstructured":"Brzozowski , J. A. 1962 . Canonical regular expressions and minimal state graphs for definite events . In Proceedings of the Symposium on Mathematical Theory of Automata. Polytechnic Institute of Brooklyn, 529--561 . Brzozowski, J. A. 1962. Canonical regular expressions and minimal state graphs for definite events. In Proceedings of the Symposium on Mathematical Theory of Automata. Polytechnic Institute of Brooklyn, 529--561."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297069"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_23"},{"key":"e_1_2_1_20_1","volume-title":"PMD Applied","author":"Copeland T.","unstructured":"Copeland , T. 2005. PMD Applied . Centennial Books . Copeland, T. 2005. PMD Applied. Centennial Books."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007515"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/514952.514955"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321651"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146254"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094841"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/222124.222146"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1028664.1028717"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the European Conference on Object Oriented Programming (ECOOP\u201901)","volume":"2072","author":"Kiczales G.","unstructured":"Kiczales , G. , Hilsdale , E. , Hugunin , J. , Kersten , M. , Palm , J. , and Griswold , W. G . 2001. An overview of AspectJ . In Proceedings of the European Conference on Object Oriented Programming (ECOOP\u201901) . Lecture Notes in Computer Science , vol. 2072 , Springer, 327--353. Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., and Griswold, W. G. 2001. An overview of AspectJ. In Proceedings of the European Conference on Object Oriented Programming (ECOOP\u201901). Lecture Notes in Computer Science, vol. 2072, Springer, 327--353."},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Kim C. H. P. Batory D. Bodden E. and Khurshid S. 2010. Reducing configurations to monitor in a software product line. In Proceedings of the 1st International Conference on Runtime Verification. Lecture Notes in Computer Science Springer. Kim C. H. P. Batory D. Bodden E. and Khurshid S. 2010. Reducing configurations to monitor in a software product line. In Proceedings of the 1st International Conference on Runtime Verification . Lecture Notes in Computer Science Springer.","DOI":"10.1007\/978-3-642-16612-9_22"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1138953.1138964"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765931.1765948"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181802"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094840"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765931.1765937"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449792"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02652-2_16"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2220365.2220366","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2220365.2220366","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:46Z","timestamp":1750276846000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2220365.2220366"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["10.1145\/2220365.2220366"],"URL":"https:\/\/doi.org\/10.1145\/2220365.2220366","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6]]},"assertion":[{"value":"2010-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}