{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:47:39Z","timestamp":1770752859366,"version":"3.50.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,5,17]],"date-time":"2005-05-17T00:00:00Z","timestamp":1116288000000},"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":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2005,7]]},"abstract":"<jats:p>We introduce the temporal logic HAWK and its supporting tool for runtime verification of Java programs. A monitor for a HAWK formula checks if a finite trace of program events satisfies the formula. HAWK is a programming-oriented extension of the rule-based EAGLE logic that has been shown capable of defining and implementing a range of finite trace monitoring logics, including future and past time temporal logic, metric (real-time) temporal logics, interval logics, forms of quantified temporal logics, extended regular expressions, state machines, and others. Monitoring is achieved on a state-by-state basis avoiding any need to store the input trace. HAWK extends EAGLE with constructs for capturing parameterized program events such as method calls and method returns. Parameters can be executing thread, the objects that methods are called upon, arguments to methods, and return values. HAWK allows one to refer to these in formulae. The tool synthesizes monitors from formulae and automates program instrumentation.<\/jats:p>","DOI":"10.1145\/1082983.1083249","type":"journal-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T19:28:32Z","timestamp":1131391712000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Event-based runtime verification of java programs"],"prefix":"10.1145","volume":"30","author":[{"given":"Marcelo","family":"d'Amorim","sequence":"first","affiliation":[{"name":"University of Illinois Urbana-Champaign"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[{"name":"Kestrel Technology, Palo Alto"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,5,17]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"4th CAV Workshops on Runtime Verification (RV'01 - RV'04)","volume":"113","year":"2001","unstructured":"1st, 2nd, 3rd, and 4th CAV Workshops on Runtime Verification (RV'01 - RV'04) , volume 55(2), 70(4), 89(2), 113 of ENTCS. Elsevier Science : 2001 , 2002, 2003, 2004. 1st, 2nd, 3rd, and 4th CAV Workshops on Runtime Verification (RV'01 - RV'04), volume 55(2), 70(4), 89(2), 113 of ENTCS. Elsevier Science: 2001, 2002, 2003, 2004."},{"key":"e_1_2_1_2_1","unstructured":"Eiffel language 2005. http:\/\/www.eiffel.com\/.  Eiffel language 2005. http:\/\/www.eiffel.com\/."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1754749.1754755"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 5th International Conference on Verification, Model Chacking, and Abstract Interpretation (VMCAI'04)","volume":"2004","author":"Barringer H.","unstructured":"H. Barringer , A. Goldberg , K. Havelund , and K. Sen . Rule-Based Runtime Verification . In Proceedings of the 5th International Conference on Verification, Model Chacking, and Abstract Interpretation (VMCAI'04) , volume 55(2), 70(4), 89(2) of LNCS, Venice, Italy, Jan 2004 . Springer. H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-Based Runtime Verification. In Proceedings of the 5th International Conference on Verification, Model Chacking, and Abstract Interpretation (VMCAI'04), volume 55(2), 70(4), 89(2) of LNCS, Venice, Italy, Jan 2004. Springer."},{"key":"e_1_2_1_5_1","series-title":"ENTCS","volume-title":"Proceedings of the First Workshop on Runtime Verification (RV'01)","author":"Bartetzko D.","year":"2001","unstructured":"D. Bartetzko , C. Fisher , M. Moller , and H. Wehrheim . Jass-Java with Assertions . In K. Havelund and G. Ro\u015fu, editors, Proceedings of the First Workshop on Runtime Verification (RV'01) , volume 55 of ENTCS , Paris, France , 2001 . Elsevier Science . D. Bartetzko, C. Fisher, M. Moller, and H. Wehrheim. Jass-Java with Assertions. In K. Havelund and G. Ro\u015fu, editors, Proceedings of the First Workshop on Runtime Verification (RV'01), volume 55 of ENTCS, Paris, France, 2001. Elsevier Science."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_31"},{"key":"e_1_2_1_7_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999","unstructured":"E. M. Clarke , O. Grumberg , and D. A. Peled . Model Checking . The MIT Press , Cambridge, Massachusetts , 1999 . E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999."},{"key":"e_1_2_1_8_1","unstructured":"M. d'Amorim and G. Ro\u015fu. Efficient Monitoring of \u03c9-languages. to appear in Computer Aided Verification (CAV'05).  M. d'Amorim and G. Ro\u015fu. Efficient Monitoring of \u03c9-languages. to appear in Computer Aided Verification (CAV'05)."},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"D.\n      Drusinsky\n    .\n  The Temporal Rover and the ATG Rover\n  . In K. Havelund J. Penix and W. Visser editors SPIN Model Checking and Software Verification volume \n  1885\n   of \n  LNCS pages \n  323\n  --\n  330\n  . \n  Springer 2000\n  .   D. Drusinsky. The Temporal Rover and the ATG Rover. In K. Havelund J. Penix and W. Visser editors SPIN Model Checking and Software Verification volume 1885 of LNCS pages 323--330. Springer 2000.","DOI":"10.1007\/10722468_19"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-51803-7_36","volume-title":"Proceedings of the 1st Conference on Temporal Logic in Specification","volume":"398","author":"Gabbay D.","year":"1987","unstructured":"D. Gabbay . The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems . In Proceedings of the 1st Conference on Temporal Logic in Specification , Altrincham , April 1987 , volume 398 of LNCS, pages 409 -- 448 , 1989. D. Gabbay. The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In Proceedings of the 1st Conference on Temporal Logic in Specification, Altrincham, April 1987, volume 398 of LNCS, pages 409--448, 1989."},{"key":"e_1_2_1_11_1","first-page":"97","volume-title":"Proceedings of the 1st International Workshop on Runtime Verification (RV'01)","author":"Havelund K.","year":"2004","unstructured":"K. Havelund and G. Ro\u015fu . Monitoring Java Programs with Java PathExplorer . In Proceedings of the 1st International Workshop on Runtime Verification (RV'01) {1}, pages 97 -- 114 . Extended version to appear in the journal: Formal Methods in System Design, Kluwer , 2004 . K. Havelund and G. Ro\u015fu. Monitoring Java Programs with Java PathExplorer. In Proceedings of the 1st International Workshop on Runtime Verification (RV'01) {1}, pages 97--114. Extended version to appear in the journal: Formal Methods in System Design, Kluwer, 2004."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053381"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/646158.680006"},{"key":"e_1_2_1_14_1","series-title":"ENTCS","volume-title":"Proceedings of Runtime Verification (RV'01)","author":"Kim M.","year":"2001","unstructured":"M. Kim , S. Kannan , I. Lee , and O. Sokolsky . Java-MaC: a Run-time Assurance Tool for Java . In Proceedings of Runtime Verification (RV'01) , volume 55 of ENTCS . Elsevier Science , 2001 . M. Kim, S. Kannan, I. Lee, and O. Sokolsky. Java-MaC: a Run-time Assurance Tool for Java. In Proceedings of Runtime Verification (RV'01), volume 55 of ENTCS. Elsevier Science, 2001."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_2_1_17_1","volume-title":"Communicating and Mobile Systems: The &pi;-Calculus","author":"Milner R.","year":"1992","unstructured":"R. Milner . Communicating and Mobile Systems: The &pi;-Calculus . Cambridge University Press , New York , 1992 . R. Milner. Communicating and Mobile Systems: The &pi;-Calculus. Cambridge University Press, New York, 1992."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/555142"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1082983.1083249","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1082983.1083249","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:14Z","timestamp":1750262894000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1082983.1083249"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5,17]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["10.1145\/1082983.1083249"],"URL":"https:\/\/doi.org\/10.1145\/1082983.1083249","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1083246.1083249","asserted-by":"subject"}]},"ISSN":["0163-5948"],"issn-type":[{"value":"0163-5948","type":"print"}],"subject":[],"published":{"date-parts":[[2005,5,17]]},"assertion":[{"value":"2005-05-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}