{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:01Z","timestamp":1776305221156,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642203978","type":"print"},{"value":"9783642203985","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-20398-5_35","type":"book-chapter","created":{"date-parts":[[2011,4,6]],"date-time":"2011-04-06T15:29:49Z","timestamp":1302103789000},"page":"472-479","source":"Crossref","is-referenced-by-count":77,"title":["OpenJML: JML for Java 7 by Extending OpenJDK"],"prefix":"10.1007","author":[{"given":"David R.","family":"Cok","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"35_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"35_CR3","series-title":"ENTCS","first-page":"73","volume-title":"Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003)","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). ENTCS, vol.\u00a080, pp. 73\u201389. Elsevier, Amsterdam (2003)"},{"key":"35_CR4","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s10009-010-0164-8","volume":"12","author":"P. Chalin","year":"2010","unstructured":"Chalin, P., Robby, James, P., Lee, J., Karabotsos, G.: Towards an industrial grade IVE for Java and next generation research platform for JML. STTT\u00a012, 429\u2013446 (2010) 10.1007\/s10009-010-0164-8","journal-title":"STTT"},{"key":"35_CR5","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) Proceedings of the International Conference on Software Engineering Research and Practice (SERP 2002), Las Vegas, Nevada, USA, June 24-27, pp. 322\u2013328. CSREA Press (2002)"},{"key":"35_CR6","unstructured":"Cochran, D., Kiniry, J.R.: Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections. In: FoVeOOS 2010 (2010)"},{"key":"35_CR7","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/s10009-010-0138-x","volume":"12","author":"D. Cok","year":"2010","unstructured":"Cok, D.: Improved usability and performance of SMT solvers for debugging specifications. STTT\u00a012, 467\u2013481 (2010)","journal-title":"STTT"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting eSC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Dietl, W., Dietzel, S., Ernst, M.D., Mu\u015flu, K., Schiller, T.: Building and using pluggable type-checkers. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Hawaii, USA, May 25\u201327 (2011)","DOI":"10.1145\/1985793.1985889"},{"key":"35_CR10","unstructured":"http:\/\/www.eclipse.org"},{"issue":"1\u20133","key":"35_CR11","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"M.D. Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming\u00a069(1\u20133), 35\u201345 (2007)","journal-title":"Science of Computer Programming"},{"key":"35_CR12","doi-asserted-by":"crossref","first-page":"2103","DOI":"10.1145\/1774088.1774531","volume-title":"Proceedings of the 2010 ACM Symposium on Applied Computing, SAC 2010","author":"M. F\u00e4hndrich","year":"2010","unstructured":"F\u00e4hndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: Proceedings of the 2010 ACM Symposium on Applied Computing, SAC 2010, pp. 2103\u20132110. ACM, New York (2010)"},{"key":"35_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for eSC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"35_CR14","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","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)"},{"key":"35_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification 2007","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Kiniry, J.R., Poll, E.: A JML tutorial: Modular specification and verification of functional behavior for Java. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, Springer, Heidelberg (2007)"},{"key":"35_CR16","unstructured":"Gary, T.: Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David\u00a0R. Cok, Peter M\u00fcller, Joseph Kiniry, Patrice Chalin, and Daniel\u00a0M. Zimmerman. JML reference manual (September 2009), http:\/\/www.jmlspecs.org"},{"key":"35_CR17","unstructured":"Rustan, K., Leino, M.: Greg Nelson, and James\u00a0B. Saxe. ESC\/Java user\u2019s manual. Technical note, Compaq Systems Research Center (October 2000)"},{"key":"35_CR18","unstructured":"http:\/\/mobius.ucd.ie"},{"key":"35_CR19","unstructured":"http:\/\/www.openjdk.org"},{"key":"35_CR20","unstructured":"Taylor, K.B., Rieken, J., Leavens, G.T.: Adapting the Java Modeling Language (JML) for Java 5 annotations. Technical Report 08-06, Department of Computer Science, Iowa State University, 226 Atanasoff Hall, Ames, Iowa 50011 (April 2008)"},{"key":"35_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-18070-5_13","volume-title":"Formal Verification of Object-Oriented Software","author":"D.M. Zimmerman","year":"2011","unstructured":"Zimmerman, D.M., Nagmoti, R.: JMLUnit: The Next Generation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 183\u2013197. Springer, Heidelberg (2011), http:\/\/formalmethods.insttech.washington.edu\/software\/jmlunitng\/"},{"key":"35_CR22","unstructured":"Why web site, http:\/\/why.lri.fr"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20398-5_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,21]],"date-time":"2021-11-21T01:48:46Z","timestamp":1637459326000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20398-5_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642203978","9783642203985"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20398-5_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}