{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T17:10:51Z","timestamp":1693847451022},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,2,16]],"date-time":"2006-02-16T00:00:00Z","timestamp":1140048000000},"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":[[2006,6]]},"DOI":"10.1007\/s10009-005-0218-5","type":"journal-article","created":{"date-parts":[[2006,2,25]],"date-time":"2006-02-25T04:15:01Z","timestamp":1140840901000},"page":"280-299","source":"Crossref","is-referenced-by-count":12,"title":["Checking JML specifications using an extensible software model checking framework"],"prefix":"10.1007","volume":"8","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","published-online":{"date-parts":[[2006,2,16]]},"reference":[{"key":"218_CR1","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning meaning to programs. In: Proceedings of the Symposium on Applied Mathematics, Mathematical Aspects of Computer Science, vol. 19, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"218_CR2","unstructured":"Meyer, B.: Object-oriented Software Construction. Prentice-Hall (1988)"},{"issue":"1","key":"218_CR3","doi-asserted-by":"crossref","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 Trans. Software Eng. 21(1), 19\u201331 (1995)","journal-title":"IEEE Trans. Software Eng."},{"key":"218_CR4","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, pp. 234\u2013245. ACM Press (2002)","DOI":"10.1145\/512529.512558"},{"key":"218_CR5","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, vol. 10, no. 2, pp. 203\u2013232. Springer-Verlag, Berlin (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"218_CR6","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Boston (1999)","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"218_CR7","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. SIGSOFT Software Engineering Notes, vol. 28, no. 5, pp. 267\u2013276. ACM Press (2003)","DOI":"10.1145\/949952.940107"},{"issue":"5","key":"218_CR8","doi-asserted-by":"crossref","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 Trans. Software Eng. 23(5), 279\u2013294 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"218_CR9","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. Electronic Notes on Theoretical Computer Science, vol. 89, no. 3. Elsevier (2003)","DOI":"10.1016\/S1571-0661(05)80009-X"},{"issue":"2\/3","key":"218_CR10","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1023\/B:FORM.0000040028.49845.67","volume":"25","author":"M.B. Dwyer","year":"2004","unstructured":"Dwyer, M.B., Hatcliff, J., Robby, Prasad, V.R.: Exploiting object escape and locking information in partial order reduction for concurrent object-oriented programs. Formal Methods Syst. Des. 25(2\/3), 199\u2013240 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"218_CR11","unstructured":"SAnToS. SpEx Website. http:\/\/spex.projects.cis.ksu.edu (2003)"},{"issue":"1","key":"218_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/9758.10500","volume":"9","author":"J.M. Wing","year":"1987","unstructured":"Wing, J.M.: Writing Larch interface language specifications. ACM Trans. Program Lang. Syst. 9(1), 1\u201324 (1987)","journal-title":"ACM Trans. Program Lang. Syst."},{"key":"218_CR13","unstructured":"Lea, D.: Concurrent Programming in Java. 2nd ed. Addison-Wesley (2000)"},{"key":"218_CR14","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Robby, Deng, X., Hatcliff, J.: Space reductions for model checking quasi-cyclic systems. In: Proceedings of the 3rd International Conference on Embedded Software (EMSOFT 2003). Lecture Notes in Computer Science, vol. 2855, pp. 173\u2013189. Springer-Verlag, Berlin (2003)","DOI":"10.1007\/978-3-540-45212-6_12"},{"key":"218_CR15","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison-Wesley (1995)"},{"key":"218_CR16","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder \u2013 a second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (2000)"},{"key":"218_CR17","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2000)"},{"key":"218_CR18","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Proceedings of The International Conference on Software Engineering Research and Practice, pp. 322\u2013328. CSREA Press (2002)"},{"key":"218_CR19","doi-asserted-by":"crossref","unstructured":"van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031, pp. 299\u2013312. Springer-Verlag, Berlin (2001)","DOI":"10.1007\/3-540-45319-9_21"},{"key":"218_CR20","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Robby, Dwyer, M.: Verifying atomicity specifications for concurrent object oriented software using model checking. In: Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937, pp. 175\u2013190. Springer-Verlag, Berlin (2004)","DOI":"10.1007\/978-3-540-24622-0_16"},{"key":"218_CR21","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.: 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. Lecture Notes in Computer Science, vol. 2852, pp. 262\u201384. Springer-Verlag, Berlin (2002)","DOI":"10.1007\/978-3-540-39656-7_11"},{"key":"218_CR22","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The slam toolkit. In: Proceedings of the 13th International Conference on Computer Aided Verification, pp. 260\u2013264. Springer-Verlag, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_25"},{"key":"218_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"218_CR24","unstructured":"Hartley, S.: Concurrent Programming \u2013 The Java Programming Language. Oxford University Press (1998)"},{"issue":"11","key":"218_CR25","doi-asserted-by":"crossref","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: Pract Exp 9(11), 1293\u20131310 (1997)","journal-title":"Concurrency: Pract Exp."},{"key":"218_CR26","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. Electronic Notes in Theoretical Computer Science, vol. 80. Elsevier (2003)","DOI":"10.1016\/S1571-0661(04)80810-7"},{"key":"218_CR27","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748\u2013752. Springer-Verlag, Saratoga, NY (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"218_CR28","unstructured":"NIII. ESC\/Java2 Website. http:\/\/www.cs.kun.nl\/sos\/research\/escjava\/index.html"},{"key":"218_CR29","doi-asserted-by":"crossref","unstructured":"Hussmann, H., Demuth, B., Finger, F.: Modular architecture for a toolset supporting OCL. In: The Third International Conference on The Unified Modeling Language. Lecture Notes in Computer Science, vol. 1939, pp. 278\u2013293. Springer-Verlag, Berlin (2000)","DOI":"10.1007\/3-540-40011-7_20"},{"key":"218_CR30","doi-asserted-by":"crossref","unstructured":"Richters, M., Gogolla, M.: Validating UML models and OCL constraints. In: The Third International Conference on The Unified Modeling Language. Lecture Notes in Computer Science, vol. 1939, pp. 265\u2013277. Springer-Verlag, Berlin (2000)","DOI":"10.1007\/3-540-40011-7_19"},{"key":"218_CR31","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, pp. 231\u2013245. ACM Press, New York, NY, USA(2002)","DOI":"10.1145\/582419.582441"},{"key":"218_CR32","doi-asserted-by":"crossref","unstructured":"Penix, J., Visser, W., Engstrom, E., Larson, A., Weininger, N.: Verification of time partitioning in the deos scheduler kernel. In: Proceedings of the 22nd International Conference on Software Engineering, pp. 488\u2013497. ACM Press (2000)","DOI":"10.1145\/337180.337364"},{"key":"218_CR33","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, pp. 116\u2013129. IEEE Computer Society (2003)","DOI":"10.1109\/ASE.2003.1240300"},{"key":"218_CR34","doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M.B.: Adapting side effects analysis for modular program model checking. In: Proceedings of the Fourth Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (2003)","DOI":"10.1145\/940071.940097"},{"key":"218_CR35","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez, E., Dwyer, M.B., Hatcliff, J., Robby.: A flexible framework for the estimation of coverage metrics in explicit state software model checking. In: Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2004). Lecture Notes in Computer Science, vol. 3362, pp. 210\u2013228. Springer-Verlag, Berlin (2004)","DOI":"10.1007\/978-3-540-30569-9_11"},{"key":"218_CR36","unstructured":"SAnToS. MAnTA Website. http:\/\/manta.projects.cis.ksu.edu (2004)"},{"key":"218_CR37","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, pp. 44\u201354. ACM Press (2002)","DOI":"10.1145\/566172.566179"},{"key":"218_CR38","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez, E., Dwyer, M., Flanagan, C., Hatcliff, J., Leavens, G.T., Robby.: Extending sequential specification techniques for modular specification and verification of multi-threaded programs. In: Proceedings of the 19th European Conference on Object-Oriented Programming (ECOOP 2005). Springer-Verlag, Berlin (in press)","DOI":"10.1007\/11531142_24"},{"key":"218_CR39","doi-asserted-by":"crossref","unstructured":"Flanagan, C.: Verifying commit-atomicity using model-checking. In: Proceedings of the 11th International SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science, vol. 2989, pp. 252\u2013266. Springer-Verlag, Berlin (2004)","DOI":"10.1007\/978-3-540-24732-6_18"}],"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-005-0218-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-005-0218-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-005-0218-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:22Z","timestamp":1559114722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-005-0218-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,2,16]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,6]]}},"alternative-id":["218"],"URL":"https:\/\/doi.org\/10.1007\/s10009-005-0218-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2,16]]}}}