{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:52:33Z","timestamp":1725573153849},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540279921"},{"type":"electronic","value":"9783540317258"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11531142_24","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T17:28:49Z","timestamp":1292866129000},"page":"551-576","source":"Crossref","is-referenced-by-count":36,"title":["Extending JML for Modular Specification and Verification of Multi-threaded Programs"],"prefix":"10.1007","author":[{"given":"Edwin","family":"Rodr\u00edguez","sequence":"first","affiliation":[]},{"given":"Matthew","family":"Dwyer","sequence":"additional","affiliation":[]},{"given":"Cormac","family":"Flanagan","sequence":"additional","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[]},{"family":"Robby","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_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. International Journal on Software Tools for Technology Transfer, STTT (2004) (to appear)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"24_CR2","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06y, Iowa State University, Department of Computer Science (2004), See, http:\/\/www.jmlspecs.org"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"G.T. Leavens","year":"2005","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming\u00a055, 185\u2013208 (2005)","journal-title":"Science of Computer Programming"},{"key":"24_CR4","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Kiniry, J.: Jml reference manual. Department of Computer Science, Iowa State University (2005), Available from http:\/\/www.jmlspecs.org"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (2004) (to appear)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"24_CR6","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-oriented Software Construction. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"24_CR7","unstructured":"SAnToS: SpEx Website (2003), http:\/\/spex.projects.cis.ksu.edu"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-540-24730-2_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Robby","year":"2004","unstructured":"Robby, Rodr\u00edguez, E., Dwyer, M., Hatcliff, J.: Checking strong specifications using an extensible software model checking framework. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 404\u2013420. Springer, Heidelberg (2004)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-24622-0_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Hatcliff","year":"2004","unstructured":"Hatcliff, J., Robby, M., Dwyer, M.: Verifying atomicity specifications for concurrent object oriented software using model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 175\u2013190. Springer, Heidelberg (2004)"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/304065.304106","volume-title":"Proceedings of the ACM 1999 Conference on Java Grande","author":"W. Pugh","year":"1999","unstructured":"Pugh, W.: Fixing the java memory model. In: Proceedings of the ACM 1999 Conference on Java Grande, New York, USA, pp. 89\u201398. ACM Press, New York (1999)"},{"key":"24_CR11","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1145\/349299.349328","volume-title":"Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation","author":"C. Flanagan","year":"2000","unstructured":"Flanagan, C., Freund, S.N.: Type-based race detection for java. In: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, New York, USA, pp. 219\u2013232. ACM Press, New York (2000)"},{"key":"24_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":"24_CR13","unstructured":"Raghavan, A.D., Leavens, G.T.: Desugaring JML method specifications. Technical Report 00-03d, Iowa State University, Department of Computer Science (2003)"},{"key":"24_CR14","unstructured":"Lerner, R.A.: Specifying Objects of Concurrent Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, TR CMU\u2013CS\u201391\u2013131 (1991)"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45337-7_1","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"J. Boyland","year":"2001","unstructured":"Boyland, J., Noble, J., Retert, W.: Capabilities for sharing. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 1\u201327. Springer, Heidelberg (2001)"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/BFb0054091","volume-title":"ECOOP \u201998 - Object-Oriented Programming","author":"J. Noble","year":"1998","unstructured":"Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol.\u00a01445, pp. 158\u2013185. Springer, Heidelberg (1998)"},{"key":"24_CR17","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A.: Universes: A type system for alias and dependency control. Technical Report 279, Fernuniversit\u00e4t Hagen, Available from (2001), http:\/\/www.informatik.fernuni-hagen.de\/pi5\/publications.html+"},{"key":"24_CR18","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.469460","volume":"21","author":"A. Borgida","year":"1995","unstructured":"Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering\u00a021, 785\u2013798 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR19","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Communications of the ACM\u00a018, 717\u2013721 (1975)","journal-title":"Communications of the ACM"},{"key":"24_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/604174.604176","volume-title":"Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Types for atomicity. In: Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 1\u201312. ACM Press, New York (2003)"},{"key":"24_CR21","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"24_CR22","doi-asserted-by":"publisher","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, R., Prasad, V.: Exploiting object escape and locking information in partial order reduction for concurrent object-oriented programs. Formal Methods in System Design\u00a025, 199\u2013240 (2004)","journal-title":"Formal Methods in System Design"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Dietl, W., M\u00fcller, P.: Universes: Lightweight ownership for jml. In: Journal of Object Technology (2005) (to appear)","DOI":"10.5381\/jot.2005.4.8.a1"},{"key":"24_CR24","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/781131.781169","volume-title":"Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp. 338\u2013349. ACM Press, New York (2003)"},{"key":"24_CR25","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/964001.964023","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 256\u2013267. ACM Press, New York (2004)"},{"key":"24_CR26","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1145\/357401.357402","volume":"2","author":"J.H. Saltzer","year":"1984","unstructured":"Saltzer, J.H., Reed, D.P., Clark, D.D.: End-to-end arguments in system design. ACM Transactions on Computer Systems\u00a02, 277\u2013288 (1984)","journal-title":"ACM Transactions on Computer Systems"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24732-6_18","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C.: Verifying commit-atomicity using model-checking. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"24_CR28","series-title":"SIGSOFT Softw. Eng. Notes.","first-page":"267","volume-title":"Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering","author":"Robby","year":"2003","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 Softw. Eng. Notes., vol.\u00a028(5), pp. 267\u2013276. ACM Press, New York (2003)"},{"key":"24_CR29","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":"24_CR30","volume-title":"Proceedings of The ACM SIGSOFT Workshop on Specification and Verification of Component Based Systems","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B., Leino, K.R.M., Schulte, W.: Verification of multithreaded object-oriented programs with invariants. In: Proceedings of The ACM SIGSOFT Workshop on Specification and Verification of Component Based Systems. ACM Press, New York (2004) (to appear)"},{"key":"24_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-39656-7_1","volume-title":"Formal Methods for Components and Objects","author":"E. \u00c1brah\u00e1m","year":"2003","unstructured":"\u00c1brah\u00e1m, E., de Boer, F.S., de Roever, W.P., Steffen, M.: A tool-supported proof system for multithreaded java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 1\u201332. Springer, Heidelberg (2003)"},{"key":"24_CR32","doi-asserted-by":"publisher","first-page":"81","DOI":"10.5381\/jot.2004.3.6.a4","volume":"3","author":"S.N. Freund","year":"2004","unstructured":"Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. Journal of Object Technology\u00a03, 81\u2013101 (2004)","journal-title":"Journal of Object Technology"},{"key":"24_CR33","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of the Third Workshop on Runtime Verification (RV)","author":"L. Wang","year":"2003","unstructured":"Wang, L., Stoller, S.D.: Run-time analysis for atomicity. In: Proceedings of the Third Workshop on Runtime Verification (RV). Electronic Notes in Theoretical Computer Science, vol.\u00a089(2). Elsevier, Amsterdam (2003)"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7\u201315 (1998)","DOI":"10.1145\/298595.298598"},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J.: Expressing checkable properties of dynamic systems: The Bandera Specification Language. In: International Journal on Software Tools for Technology Transfer, vol.\u00a04, pp. 34\u201356 (2002)","DOI":"10.1007\/s100090200075"},{"key":"24_CR36","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1145\/581339.581394","volume-title":"Proceedings of the 24th International Conference on Software Engineering (ICSE 2002)","author":"X. Deng","year":"2002","unstructured":"Deng, X., Dwyer, M.B., Hatcliff, J., Mizuno, M.: Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In: Proceedings of the 24th International Conference on Software Engineering (ICSE 2002), pp. 442\u2013452. ACM Press, New York (2002)"},{"key":"24_CR37","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, June 2002, pp. 322\u2013328. CSREA Press (2002)"},{"key":"24_CR38","unstructured":"SAnToS: JMLEclipse Website (2004), http:\/\/jmleclipse.projects.cis.ksu.edu"},{"key":"24_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2005 - Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11531142_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:08:47Z","timestamp":1605643727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11531142_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540279921","9783540317258"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/11531142_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}