{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T02:36:39Z","timestamp":1784342199680,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540434191","type":"print"},{"value":"9783540460022","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46002-0_24","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T02:29:59Z","timestamp":1193538599000},"page":"342-356","source":"Crossref","is-referenced-by-count":215,"title":["Synthesizing Monitors for Safety Properties"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Manuel Clavel, Steven Eker, Patrick Lincoln, and Jos\u00e9 Meseguer. Principles of Maude. In Jos\u00e9 Meseguer, editor, Proceedings, First International Workshop on Rewriting Logic and its Applications. Elsevier Science, 1996. Volume 4, Electronic Notes in Theoretical Computer Science.","DOI":"10.1016\/S1571-0661(04)00034-9"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"James Corbett, Matthew B. Dwyer, John Hatcliff, Corina S. Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. 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.","DOI":"10.1145\/337180.337234"},{"issue":"7","key":"24_CR3","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. Demartini","year":"1999","unstructured":"Claudio Demartini, Radu Iosif, and Riccardo Sisto. A Deadlock Detection Tool for Concurrent Java Programs. Software Practice and Experience, 29(7):577\u2013603, July 1999.","journal-title":"Software Practice and Experience"},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/10722468_19","volume-title":"SPIN Model Checking and Software Verification","author":"D. Drusinsky","year":"2000","unstructured":"Doron Drusinsky. The Temporal Rover and the ATG Rover. In Klaus Havelund, John Penix, and Willem Visser, editors, SPIN Model Checking and Software Verification, volume 1885 of Lecture Notes in Computer Science, pages 323\u2013330. Springer, 2000."},{"key":"24_CR5","unstructured":"Klaus Havelund, Scott Johnson, and Grigore Rosu. Specification and Error Pattern Based Program Monitoring. In European Space Agency Workshop on On-Board Autonomy, Noordwijk, The Netherlands, 2001."},{"issue":"8","key":"24_CR6","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K. Havelund","year":"2001","unstructured":"Klaus Havelund, Michael Lowry, and John Penix. Formal Analysis of a Space Craft Controller using SPIN. IEEE Transactions on Software Engineering, 27(8):749\u2013765, August 2001.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"24_CR7","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Klaus Havelund and Thomas Pressburger. Model Checking Java Programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4):366\u2013381, April 2000. Special issue of STTT containing selected submissions to the 4th SPIN workshop, Paris, France, 1998.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"24_CR8","unstructured":"Klaus Havelund and Grigore Rosu. Java PathExplorer-A Runtime Verification Tool. In The 6th International Symposium on Arti.cial Intelligence, Robotics and Automation in Space: A New Space Odyssey, Montreal, Canada, June 18\u201321, 2001."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Klaus Havelund and Grigore Rosu. Monitoring Java Programs with Java PathExplorer. In Klaus Havelund and Grigore Rosu, editors, Proceedings of Runtime Verification (RV\u201901), volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001.","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Klaus Havelund and Grigore Rosu. Monitoring Programs using Rewriting. In Proceedings, International Conference on Automated Software Engineering (ASE\u201901), pages 135\u2013143. Institute of Electrical and Electronics Engineers, 2001. San Diego, California.","DOI":"10.1109\/ASE.2001.989799"},{"key":"24_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"FME\u201996: Industrial Benefit and Advances in Formal Methods","author":"K. Havelund","year":"1996","unstructured":"Klaus Havelund and Natarajan Shankar. Experiments in Theorem Proving and Model Checking for Protocol Veri.cation. In Marie Claude Gaudel and Jim Woodcock, editors, FME\u201996: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 662\u2013681. Springer, 1996."},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Gerard J. Holzmann and Margaret H. Smith. A Practical Method for Verifying Event-Driven Software. In Proceedings of ICSE\u201999, International Conference on Software Engineering, Los Angeles, California, USA, May 1999. IEEE\/ACM.","DOI":"10.1145\/302405.302710"},{"key":"24_CR13","unstructured":"JavaCC. Web page. http:\/\/www.webgain.com\/products\/java_cc ."},{"key":"24_CR14","unstructured":"JTrek. Web page. http:\/\/www.compaq.com\/java\/download ."},{"key":"24_CR15","unstructured":"Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, and Mahesh Viswanathan. Runtime Assurance Based on Formal Specifications. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999."},{"key":"24_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, 1992."},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"David Y.W. Park, Ulrich Stern, and David L. Dill. Java Model Checking. In Proceedings of the First International Workshop on Automated Program Analysis, Testing and Verification, Limerick, Ireland, June 2000.","DOI":"10.1109\/ASE.2000.873671"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46\u201377, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"24_CR19","unstructured":"Grigore Rosu and Klaus Havelund. Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae. Technical Report TR 01-08, NASA\u2014RIACS, May 2001."},{"key":"24_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/10722468_14","volume-title":"SPIN Model Checking and Software Verification","author":"S. D. Stoller","year":"2000","unstructured":"Scott D. Stoller. Model-Checking Multi-threaded Distributed Java Programs. In Klaus Havelund, John Penix, and Willem Visser, editors, SPIN Model Checking and Software Verification, volume 1885 of Lecture Notes in Computer Science, pages 224\u2013244. Springer, 2000."},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Willem Visser, Klaus Havelund, Guillaume Brat, and SeungJoon Park. Model Checking Programs. In Proceedings of ASE\u20192000: The 15th IEEE International Conference on Automated Software Engineering. IEEE CS Press, September 2000.","DOI":"10.1109\/ASE.2000.873645"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46002-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:29:11Z","timestamp":1556922551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46002-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434191","9783540460022"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-46002-0_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}