{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:23:00Z","timestamp":1742383380350},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212997"},{"type":"electronic","value":"9783540247302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_31","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T15:00:15Z","timestamp":1280761215000},"page":"404-420","source":"Crossref","is-referenced-by-count":12,"title":["Checking Strong Specifications Using an Extensible Software Model Checking Framework"],"prefix":"10.1007","author":[{"family":"Robby","sequence":"first","affiliation":[]},{"given":"Edwin","family":"Rodr\u00edguez","sequence":"additional","affiliation":[]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (2003)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"31_CR2","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the java modeling language. In: Proceedings of the International Conference on Software Engineering Research and Practice (2002)"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Hatcliff, J., Prasad, V.R., Robby: Exploiting object escape and locking information in partial order reductions for concurrent object-oriented programs. Formal Methods in System Designs (2004) (to appear)","DOI":"10.1023\/B:FORM.0000040028.49845.67"},{"issue":"11","key":"31_CR4","doi-asserted-by":"publisher","first-page":"1293","DOI":"10.1002\/(SICI)1096-9128(199711)9:11<1293::AID-CPE340>3.0.CO;2-J","volume":"9","author":"M.B. Dwyer","year":"1997","unstructured":"Dwyer, M.B., Wallentine, V.: A framework for parallel adaptive grid simulations. Concurrency: Practice and Experience\u00a09(11), 1293\u20131310 (1997)","journal-title":"Concurrency: Practice and Experience"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation (2002)","DOI":"10.1145\/512529.512558"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning meaning to programs. In: Proceedings of the Symposium on Applied Mathematics (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"31_CR7","volume-title":"Concurrent Programming - The Java Programming Language","author":"S. Hartley","year":"1998","unstructured":"Hartley, S.: Concurrent Programming - The Java Programming Language. Oxford University Press, Oxford (1998)"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Robby, Dwyer, M.B.: Verifying atomicity specifications for concurrent objectoriented software using model checking. In: Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (January 2004)","DOI":"10.1007\/978-3-540-24622-0_16"},{"issue":"5","key":"31_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013294 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/3-540-40011-7_20","volume-title":"UML 2000 - The Unified Modeling Language. Advancing the Standard","author":"H. Hussmann","year":"2000","unstructured":"Hussmann, H., Demuth, B., Finger, F.: Modular architecture for a toolset supporting OCL. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol.\u00a01939, pp. 278\u2013293. Springer, Heidelberg (2000)"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Marinov, D., Jackson, D.: An analyzable annotation language. In: Proceedings of the 17th ACM conference on Object-oriented programming, systems, languages, and applications (2002)","DOI":"10.1145\/582419.582441"},{"key":"31_CR12","volume-title":"Concurrent Programming in Java:","author":"D. Lea","year":"2000","unstructured":"Lea, D.: Concurrent Programming in Java: 2nd edn. Addison-Wesley, Reading (2000)","edition":"2"},{"key":"31_CR13","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java modeling language. In: Formal Underpinnings of Java Workshop (October 1998)"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C.: How the design of JML accommodates both runtime assertion checking and formal verification. In: Proceedings of the 1st International Symposium on Formal Methods for Components and Objects (November 2002)","DOI":"10.1007\/978-3-540-39656-7_11"},{"key":"31_CR15","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer, B.: Object-oriented Software Construction. Prentice-Hall, Englewood Cliffs (1988)"},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, Springer, Heidelberg (1992)"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-40011-7_19","volume-title":"UML 2000 - The Unified Modeling Language. Advancing the Standard","author":"M. Richters","year":"2000","unstructured":"Richters, M., Gogolla, M.: Validating UML models and OCL constraints. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol.\u00a01939, pp. 265\u2013277. Springer, Heidelberg (2000)"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2003)","DOI":"10.1145\/940071.940107"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor Website (2003), http:\/\/bogor.projects.cis.ksu.edu","DOI":"10.1145\/949952.940107"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J., Iosif, R.: Space-reduction strategies for model checking dynamic systems. In: Proceedings of the 2003 Workshop on Software Model Checking (July 2003)","DOI":"10.1007\/978-3-540-45212-6_12"},{"issue":"1","key":"31_CR21","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/32.341844","volume":"21","author":"D.S. Rosenblum","year":"1995","unstructured":"Rosenblum, D.S.: A practical approach to programming with assertions. IEEE Transactions on Software Engineering\u00a021(1), 19\u201331 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"Stoller, S.D.: Domain partitioning for open reactive systems. In: Proceedings of the International Symposium on Software Testing and Analysis (2002)","DOI":"10.1145\/566172.566179"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M., Pasareanu, C.: Automated environment generation for software model checking. In: Proceedings of the 18th International Conference on Automated Software Engineering (October 2003)","DOI":"10.1109\/ASE.2003.1240300"},{"key":"31_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 299. Springer, Heidelberg (2001)"},{"key":"31_CR25","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proceedings of the 15th IEEE Conference on Automated Software Engineering (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\/978-3-540-24730-2_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T03:18:11Z","timestamp":1559359091000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}