{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:36:22Z","timestamp":1725539782890},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642045691"},{"type":"electronic","value":"9783642045707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04570-7_10","type":"book-chapter","created":{"date-parts":[[2009,11,2]],"date-time":"2009-11-02T23:51:23Z","timestamp":1257205883000},"page":"117-132","source":"Crossref","is-referenced-by-count":0,"title":["Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs"],"prefix":"10.1007","author":[{"given":"Pavel","family":"Parizek","sequence":"first","affiliation":[]},{"given":"Tomas","family":"Kalibera","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/11785477_7","volume-title":"ECOOP 2006 \u2013 Object-Oriented Programming","author":"C. Andreae","year":"2006","unstructured":"Andreae, C., Coady, Y., Gibbs, C., Noble, J., Vitek, J., Zhao, T.: Scoped Types and Aspects for Real-Time Java. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol.\u00a04067, pp. 124\u2013147. Springer, Heidelberg (2006)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/978-3-540-27813-9_42","volume-title":"Computer Aided Verification","author":"T. Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A Model Checker for Concurrent Software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 484\u2013487. Springer, Heidelberg (2004)"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Armbuster, A., Baker, J., Cunei, A., Flack, C., Holmes, D., Pizlo, F., Pla, E., Prochazka, M., Vitek, J.: A Real-Time Java Virtual Machine for Avionics. ACM Transactions on Embedded Computing Systems\u00a07(1) (2007)","DOI":"10.1145\/1324969.1324974"},{"key":"10_CR4","series-title":"Java Series","volume-title":"The Real-Time Specification for Java","author":"G. Bollella","year":"2000","unstructured":"Bollella, G., Gosling, J., Brosgol, B., Dibble, P., Furr, S., Turnbull, M.: The Real-Time Specification for Java. Java Series. Addison-Wesley, Reading (2000)"},{"key":"10_CR5","unstructured":"CLDC HotSpot Implementation Virtual Machine, White Paper, Sun Microsystems, http:\/\/java.sun.com\/products\/cldc\/wp\/CLDC_HI_WhitePaper.pdf (accessed in March 2009)"},{"key":"10_CR6","volume-title":"Proceedings of the 8th ACM Workshop on Program Analysis for Software Tools and Engineering (PASTE 2008)","author":"A. De","year":"2008","unstructured":"De, A., Roychoudhury, A., D\u2019Souza, D.: Java Memory Model aware Software Validation. In: Proceedings of the 8th ACM Workshop on Program Analysis for Software Tools and Engineering (PASTE 2008). ACM Press, New York (2008)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/11513988_15","volume-title":"Computer Aided Verification","author":"M.B. Dwyer","year":"2005","unstructured":"Dwyer, M.B., Hatcliff, J., Hoosier, M., Robby: Building Your Own Software Model Checker Using The Bogor Extensible Model Checking Framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 148\u2013152. Springer, Heidelberg (2005)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"10_CR9","volume-title":"The Java Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)","edition":"3"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: Heuristics for Model Checking Java Programs. International Journal on Software Tools for Technology Transfer\u00a06(4) (2004)","DOI":"10.1007\/s10009-003-0130-9"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11813040_32","volume-title":"FM 2006: Formal Methods","author":"T.Q. Huynh","year":"2006","unstructured":"Huynh, T.Q., Roychoudhury, A.: A Memory Model Sensitive Checker for C#. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 476\u2013491. Springer, Heidelberg (2006)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"IBM J9 Java Virtual Machine, http:\/\/wiki.eclipse.org\/index.php\/J9 (accessed March 2009)","DOI":"10.1111\/j.1479-8301.2009.00287.x"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Iosif, R.: Symmetry Reductions for Model Checking of Concurrent Dynamic Software. International Journal on Software Tools for Technology Transfer (STTT)\u00a06(4) (2004)","DOI":"10.1007\/s10009-004-0154-9"},{"key":"10_CR14","unstructured":"Jikes RVM (Research Virtual Machine), http:\/\/jikesrvm.org (accessed in March 2009)"},{"key":"10_CR15","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Prentice Hall, Englewood Cliffs (1999)","edition":"2"},{"key":"10_CR16","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2007)","author":"M. Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative Context Bounding for Systematic Testing of Multithreaded Programs. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2007). ACM Press, New York (2007)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-642-03240-0_7","volume-title":"FMICS 2008","author":"R. Pelanek","year":"2009","unstructured":"Pelanek, R.: Fighting State Space Explosion: Review and Evaluation. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol.\u00a05596, pp. 37\u201352. Springer, Heidelberg (2009)"},{"key":"10_CR18","volume-title":"Proceedings of the 7th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2004)","author":"F. Pizlo","year":"2004","unstructured":"Pizlo, F., Fox, J., Holmes, D., Vitek, J.: Real-time Java Scoped Memory: Design patterns and Semantics. In: Proceedings of the 7th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2004). IEEE CS, Los Alamitos (2004)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-Bounded Model Checking of Concurrent Software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded Model Checking of Concurrent Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 82\u201397. Springer, Heidelberg (2005)"},{"key":"10_CR21","unstructured":"The Scala Programming Language, http:\/\/www.scala-lang.org\/ (accessed in March 2009)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-540-70592-5_6","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"S. Srinivasan","year":"2008","unstructured":"Srinivasan, S., Mycroft, A.: Kilim: Isolation-Typed Actors for Java. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 104\u2013128. Springer, Heidelberg (2008)"},{"key":"10_CR23","unstructured":"Sun Java SE HotSpot, Sun Microsystems, http:\/\/java.sun.com\/javase\/technologies\/hotspot\/ (accessed in March 2009)"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering Journal\u00a010(2) (2003)","DOI":"10.1023\/A:1022920129859"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenstrom, P.: The Worst-Case Execution-Time Problem - Overview of Methods and Survey of Tools. ACM Transactions on Embedded Computing Systems\u00a07(3) (2008)","DOI":"10.1145\/1347375.1347389"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04570-7_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:42:31Z","timestamp":1606167751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04570-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642045691","9783642045707"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04570-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}