{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:04:59Z","timestamp":1748070299938},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664994"},{"type":"electronic","value":"9783540482345"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48234-2_17","type":"book-chapter","created":{"date-parts":[[2007,10,29]],"date-time":"2007-10-29T23:58:10Z","timestamp":1193702290000},"page":"216-231","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Applying Model Checking in Java Verification"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Jens Ulrik","family":"Skakkeb\u00e6k","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,8,27]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM\/IEEE Design Automation Conference, 1990.","DOI":"10.1145\/123186.123223"},{"key":"17_CR2","unstructured":"R. Iosif C. Demartini and R. Sisto. Modeling and Validation of Java Multithreading Applications using SPIN. In G. Holzmann, E. Najm, and A. S erhrouchni, editors, Proceedings of the 4th SPIN workshop, Paris, France, November 1998."},{"key":"17_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, Portugal","author":"Cattel. T","year":"1998","unstructured":"T. Cattel. Modeling and Verification of sC++ Applications. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, Portugal, LNCS 1384, April 1998."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"J. C. Corbett. Constructing Compact Models of Concurrent Java Programs. In Proceedings of the ACM Sigsoft Symposium on Software Testing and Analysis, Clearwater Beach, Florida., March 1998.","DOI":"10.1145\/271771.271778"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. ACM Symposium on Principles of Programming Languages, pages 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"W. de Roever, H. Langmaack, and A. Pnueli (Eds.). Compositionality: The Significant Difference, International Symposium, COMPOS\u201997, Bad Malente, Germany. LNCS 1536. Springer-Verlag, September 1997.","DOI":"10.1007\/3-540-49213-5"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"P. Godefroid. Model checking for programming languages using Verisoft. In ACM Symposium on Principles of Programming Languages, pages 174\u2013186, Paris, January 1997.","DOI":"10.1145\/263699.263717"},{"key":"17_CR8","unstructured":"J. Gosling, B. J oy, and G. Steele. The Java Language Specification. The Java Series. A-W, 1996."},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, CAV. Springer-Verlag, June 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"J. Hatcli-, M. Dwyer, S. Laubach, and D. Schmidt. Stating static analysis using abstraction-based program specialization, 1998.","DOI":"10.1007\/BFb0056612"},{"key":"17_CR11","unstructured":"K. Havelund, M. Lowry, and J. Penix. Formal Analysis of a Space Craft Controller using SPIN. In G. Holzmann, E. Najm, and A. Serhrouchni, editors, Proceedings of the 4th SPIN workshop, Paris, France, November 1998."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger. Model Checking Java Programs using Java PathFinder. NASA Ames Research Center. To appear in the International Journal on Software Tools for Technology Transfer (STTT), 1999.","DOI":"10.1007\/s100090050043"},{"key":"17_CR13","unstructured":"Gerard Holzmann. The Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"N. D. Jones, editor. Special Issue on Partial Evaluation, 1993 (Journal of Functional Programming, vol. 3, no. 4). Cambridge University Press, 1993.","DOI":"10.1017\/S0956796800000812"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"G. Naumovich, G.S. Avrunin, and L.A. Clarke. Data flow analysis for checking properties of concurrent java programs. Technical Report 98-22, Computer Science Department, University of Massachusetts at Amherst, April 1998.","DOI":"10.1145\/302405.302663"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"B. Pell, E. Gat, R. Keesing, N. Muscettola, and B. S mith. Plan Execution for Autonomous Spacecrafts. In Proceedings of the 1997 International Joint Conference on Artificial Intelligence, 1997.","DOI":"10.1145\/267658.267724"},{"issue":"3","key":"17_CR18","first-page":"121","volume":"3","author":"Tip. F","year":"1995","unstructured":"F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121\u2013189, 1995.","journal-title":"Journal of Programming Languages"}],"container-title":["Lecture Notes in Computer Science","Theoretical and Practical Aspects of SPIN Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48234-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T11:29:52Z","timestamp":1684063792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48234-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664994","9783540482345"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48234-2_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"27 August 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}