{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,18]],"date-time":"2026-02-18T22:46:13Z","timestamp":1771454773530,"version":"3.50.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2003,11,28]],"date-time":"2003-11-28T00:00:00Z","timestamp":1069977600000},"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":[[2004,8]]},"DOI":"10.1007\/s10009-003-0117-6","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T03:37:25Z","timestamp":1079753845000},"page":"158-173","source":"Crossref","is-referenced-by-count":106,"title":["Efficient monitoring of safety properties"],"prefix":"10.1007","volume":"6","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,11,28]]},"reference":[{"key":"117_CR1","doi-asserted-by":"crossref","unstructured":"Artho C, Drusinsky D, Goldberg A, Havelund K, Lowry M, Pasareanu C, Ro\u015fu G, Visser W (2003) Experiments with test case generation and runtime analysis. In: B\u00f6rger E, Gargantini A, Riccobene E (eds) Proceedings of Abstract State Machines 2003, Taormina, Italy, March 2003. Lecture notes in computer science, vol 2589. Springer, Berlin Heidelberg New York, pp 87\u2013107","DOI":"10.1007\/3-540-36498-6_5"},{"key":"117_CR2","doi-asserted-by":"crossref","unstructured":"Artho C, Havelund K, Biere A (2003) High-level data races. In: Proceedings of the 1st international workshop on verification and validation of enterprise information systems (VVEIS\u201903), Angers, France, April 2003","DOI":"10.1002\/stvr.281"},{"key":"117_CR3","doi-asserted-by":"crossref","unstructured":"Ball T, Podelski A, Rajamani S (2001) Boolean and Cartesian abstractions for model checking C programs. In: Proceedings of tools and algorithms for the construction and analysis of systems (TACAS\u201901), Genoa, Italy, April 2001. Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York, pp 268\u2013283","DOI":"10.1007\/3-540-45319-9_19"},{"key":"117_CR4","doi-asserted-by":"crossref","unstructured":"Chen F, Ro\u015fu G (2003) Towards monitoring-oriented programming: a paradigm combining specification and implementation. In: Proceedings of the 3rd workshop on runtime verification (RV\u201903), Boulder, CO, July 2003. Electronic notes in theoretical computer science, vol 89. Elsevier, Amsterdam, pp 106\u2013125","DOI":"10.1016\/S1571-0661(04)81045-4"},{"key":"117_CR5","doi-asserted-by":"crossref","unstructured":"Clavel M, Dur\u00e1n FJ, Eker S, Lincoln P, Mart\u00ed-Oliet N, Meseguer J, Quesada JF (1999) Maude: specification and programming in rewriting logic. Maude System documentation at http:\/\/maude.csl.sri.com\/papers","DOI":"10.1007\/3-540-48685-2_18"},{"key":"117_CR6","doi-asserted-by":"crossref","unstructured":"Clavel M, Dur\u00e1n FJ, Eker S, Lincoln P, Mart\u00ed-Oliet N, Meseguer J, Quesada JF (1999) The Maude system. In: Narendran P, Rusinowitch M (eds) Proceedings of the 10th international conference on rewriting techniques and applications (RTA-99), Trento, Italy, July 1999. Lecture notes in computer science, vol 1631. Springer, Berlin Heidelberg New York, pp 240\u2013243","DOI":"10.1007\/3-540-48685-2_18"},{"key":"117_CR7","unstructured":"Clavel M, Dur\u00e1n FJ, Eker S, Lincoln P, Mart\u00ed-Oliet N, Meseguer J, Quesada JF (2000) A Maude tutorial. Manuscript at: http:\/\/maude.csl.sri.com\/papers"},{"key":"117_CR8","doi-asserted-by":"crossref","unstructured":"Corbett J, Dwyer MB, Hatcliff J, Pasareanu CS, Robby Laubach S, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: Proceedings of the 22nd international conference on software engineering, Limerick, Ireland, June 2000. ACM Press, New York, pp 439\u2013448","DOI":"10.1145\/337180.337234"},{"key":"117_CR9","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"Demartini","year":"1999","unstructured":"Demartini C, Iosif R, Sisto R (1999) A deadlock detection tool for concurrent Java programs. Software Pract Exper 29(7):577\u2013603","journal-title":"Software Pract Exper"},{"key":"117_CR10","doi-asserted-by":"crossref","unstructured":"Drusinsky D (2000) The Temporal Rover and the ATG Rover. In: Havelund K, Penix J, Visser W (eds) SPIN model checking and software verification. Lecture notes in computer science, vol 1885. Springer, Berlin Heidelberg New York, pp 323\u2013330","DOI":"10.1007\/10722468_19"},{"key":"117_CR11","doi-asserted-by":"crossref","unstructured":"Gabbay DM (1989) The declarative past and imperative future: executable temporal logic for interactive systems. In: Banieqbal B, Barringer H, Pnueli A (eds) Proceedings of the 1st conference on temporal logic in specification, Altrincham, UK, April 1989. Lecture notes in computer science, vol 398. Springer, Berlin Heidelberg New York, pp 409\u2013448","DOI":"10.1007\/3-540-51803-7_36"},{"key":"117_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid P (1997) Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM symposium on principles of programming languages, Paris, France, January 1997. ACM Press, New York, pp 174\u2013186","DOI":"10.1145\/263699.263717"},{"key":"117_CR13","doi-asserted-by":"crossref","unstructured":"Gunter E, Peled D (2002) Tracing the executions of concurrent programs. In: Havelund K, Ro\u015fu G (eds) Proceedings of runtime verification (RV\u201902), Copenhagen, July 2002. Electronic notes in theoretical computer science, vol 70. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(04)80581-4"},{"key":"117_CR14","unstructured":"Havelund K, Johnson S, Ro\u015fu G (2001) Specification and error pattern based program monitoring. In: Proceedings of the European Space Agency workshop on on-board autonomy, Noordwijk, The Netherlands, October 2001, pp 323\u2013330"},{"key":"117_CR15","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"Havelund","year":"2001","unstructured":"Havelund K, Lowry M, Penix J (2001) Formal analysis of a space craft controller using SPIN. IEEE Trans Software Eng 27(8):749\u2013765","journal-title":"IEEE Trans Software Eng"},{"key":"117_CR16","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"Havelund","year":"1998","unstructured":"Havelund K, Pressburger T (1998) Model checking Java programs using Java PathFinder. Int J Software Tools Technol Trans 2(4):366\u2013381. Special issue of STTT containing selected submissions to the 4th SPIN workshop, Paris, France, November 1998","journal-title":"Int J Software Tools Technol Trans"},{"key":"117_CR17","unstructured":"Havelund K, Ro\u015fu G (2001a) Java PathExplorer \u2013 a runtime verification tool. In: Proceedings of the 6th international symposium on artificial intelligence, robotics and automation in space: a new space odyssey, Montreal, 18\u201321 June 2001. Canadian Space Agency. Paper AM126 on CD-ROM"},{"key":"117_CR18","doi-asserted-by":"crossref","unstructured":"Havelund K, Ro\u015fu G (2001b) Monitoring Java programs with Java PathExplorer. In: Havelund K, Ro\u015fu G (eds) Proceedings of Runtime Verification (RV\u201901), Paris, July 2001. Electronic notes in theoretical computer science, vol 55. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"117_CR19","doi-asserted-by":"crossref","unstructured":"Havelund K, Ro\u015fu G (2001c) Monitoring programs using rewriting. In: Proceedings of the international conference on automated software engineering (ASE\u201901). Institute of Electrical and Electronics Engineers. Coronado Island, CA, November 2001, pp 135\u2013143","DOI":"10.1109\/ASE.2001.989799"},{"key":"117_CR20","doi-asserted-by":"crossref","unstructured":"Havelund K, Shankar N (1996) Experiments in theorem proving and model checking for protocol verification. In: Gaudel MC, Woodcock J (eds) Proceedings of FME\u201996: Industrial Benefit and Advances in Formal Methods, Oxford, UK, March 1996. Lecture notes in computer science, vol 1051. Springer, Berlin Heidelberg New York, pp 662\u2013681","DOI":"10.1007\/3-540-60973-3_113"},{"key":"117_CR21","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Software Eng 23(5):279\u2013295 1997. Special issue on formal methods in software practice","journal-title":"IEEE Trans Software Eng"},{"key":"117_CR22","doi-asserted-by":"crossref","unstructured":"Holzmann GJ, Smith MH (1999) A practical method for verifying event-driven software. In: Proceedings of the international conference on software engineering (ICSE\u201999), Los Angeles, May 1999. IEEE\/ACM Press, New York, pp 597\u2013607","DOI":"10.1145\/302405.302710"},{"key":"117_CR23","unstructured":"Hsiang J (1981) Refutational theorem proving using term rewriting systems. PhD thesis, University of Illinois at Champaign-Urbana"},{"key":"117_CR24","unstructured":"JavaCC. Available at: http:\/\/www.webgain.com\/products\/java_cc"},{"key":"117_CR25","unstructured":"JTrek. Available at: http:\/\/www.compaq.com\/java\/download"},{"key":"117_CR26","unstructured":"Lee I, Kannan S, Kim M, Sokolsky O, Viswanathan M (1999) Runtime assurance based on formal specifications. In: Proceedings of the international conference on parallel and distributed processing techniques and applications, Las Vegas, USA, June 1999. CSREA Press"},{"key":"117_CR27","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"117_CR28","first-page":"safety","volume":"systems","author":"Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin Heidelberg New York","journal-title":"Temporal verification of reactive"},{"key":"117_CR29","first-page":"122","volume":"79","author":"Markey","year":"2003","unstructured":"Markey N (2003) Temporal logic with past is exponentially more succinct. EATCS Bull 79:122\u2013128","journal-title":"EATCS Bull"},{"key":"117_CR30","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"1","author":"Meseguer","year":"1992","unstructured":"Meseguer J (1992) Conditional rewriting logic as a unified model of concurrency. Theor Comput Sci 1:73\u2013155","journal-title":"Theor Comput Sci"},{"key":"117_CR31","unstructured":"Meseguer J (1997) Membership algebra as a logical framework for equational specification. In: Proceedings of the workshop on algebraic development techniques (WADT\u201997), Tarquinia, Italy, June 1998. Lecture notes in computer science, vol 1376. Springer, Berlin Heidelberg New York, pp 18\u201361"},{"key":"117_CR32","doi-asserted-by":"crossref","unstructured":"Park DY, Stern U, Skakkebaek JU, Dill DL (2000) Java model checking. In: Proceedings of the automated software engineering conference, Grenoble, France, September 2000. IEEE Computer Society, New York, pp 253\u2013256","DOI":"10.1109\/ASE.2000.873671"},{"key":"117_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium on foundations of computer science, Providence, RI, October 1977, pp 46\u201377","DOI":"10.1109\/SFCS.1977.32"},{"key":"117_CR34","unstructured":"Ro\u015fu G, Havelund K (2001) Synthesizing dynamic programming algorithms from linear temporal logic formulae. Technical Report TR 01-08, NASA \u2013 RIACS, Moffett Field, CA"},{"key":"117_CR35","doi-asserted-by":"crossref","unstructured":"Sen K, Ro\u015fu G, Agha G (2003) Runtime safety analysis of multithreaded programs. In: Proceedings of the 4th joint European software engineering conference and ACM SIGSOFT symposium on the foundations of software engineering (ESEC\/FSE\u201903), Helsinki, September 2003. ACM Press, New York","DOI":"10.1145\/940071.940116"},{"key":"117_CR36","doi-asserted-by":"crossref","unstructured":"Stoller SD (2000) Model-checking multi-threaded distributed Java programs. In: Havelund K, Penix J, Visser W (eds) SPIN model checking and software verification. Lecture notes in computer science, vol 1885. Springer, Berlin Heidelberg New York, pp 224\u2013244","DOI":"10.1007\/10722468_14"},{"key":"117_CR37","doi-asserted-by":"crossref","unstructured":"Visser W, Havelund K, Brat G, Park S (2000) Model checking programs. In: Proceedings of the 15th IEEE international conference on automated software engineering (ASE\u20192000), Grenoble, France, September 2000. IEEE Press, New York, pp 3\u201312","DOI":"10.1109\/ASE.2000.873645"}],"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-003-0117-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0117-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0117-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T18:05:22Z","timestamp":1585677922000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0117-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,11,28]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["117"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0117-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,11,28]]}}}