{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:07:30Z","timestamp":1757311650339},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_18","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"246-261","source":"Crossref","is-referenced-by-count":11,"title":["JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity"],"prefix":"10.1007","author":[{"given":"Patrice","family":"Chalin","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Rioux","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"18_CR1","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","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. International Journal on Soft-ware Tools for Technology Transfer (STTT)\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Soft-ware Tools for Technology Transfer (STTT)"},{"key":"18_CR2","unstructured":"Chalin, P.: Reassessing JML\u2019s Logical Foundation. In: Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP 2005), Glasgow, Scotland (July 2005)"},{"issue":"2","key":"18_CR3","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/s00165-006-0016-1","volume":"19","author":"P. Chalin","year":"2007","unstructured":"Chalin, P.: Are the Logical Foundations of Verifying Compiler Prototypes Matching User Ex-pectations? Formal Aspects of Computing\u00a019(2), 139\u2013158 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Chalin, P.: A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler. In: Proceedings of the Int\u2019l Conf. on Soft. Eng. (ICSE), pp. 23\u201333 (2007)","DOI":"10.1109\/ICSE.2007.9"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Chalin, P., James, P.R.: Non-null References by Default in Java: Alleviating the Nullity Annotation Burden. In: Proceedings of the ECOOP, pp. 227\u2013247 (2007)","DOI":"10.1007\/978-3-540-73589-2_12"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J., Leavens, G.T., Poll, E.: Beyond Assertions: Advanced Specification and Verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"18_CR7","unstructured":"Cheon, Y.: A Runtime Assertion Checker for the Java Modeling Language., Iowa State Uni-versity, Ph.D. Thesis, also TR #03-09 (April 2003)"},{"key":"18_CR8","first-page":"231","volume-title":"Proceedings of the ECOOP","author":"Y. Cheon","year":"2002","unstructured":"Cheon, Y., Leavens, G.T.: A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In: Proceedings of the ECOOP, pp. 231\u2013255. Springer, Heidelberg (2002)"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Cheon, Y., Leavens, G.T.: A Contextual Interpretation Of Undefinedness For Runtime Assertion Checking. In: Proc. Int\u2019l Symp. on Automated Analysis-driven Debugging (2005)","DOI":"10.1145\/1085130.1085150"},{"issue":"3","key":"18_CR10","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/1127878.1127900","volume":"31","author":"L.A. Clarke","year":"2006","unstructured":"Clarke, L.A., Rosenblum, D.S.: A Historical Perspective on Runtime Assertion Checking in Software Development. ACM SIGSOFT SEN\u00a031(3), 25\u201337 (2006)","journal-title":"ACM SIGSOFT SEN"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"18_CR12","volume-title":"Design Patterns: Elements of Reusable Ob-ject-Oriented Software","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Ob-ject-Oriented Software. Addison-Wesley, Reading (1995)"},{"issue":"3","key":"18_CR13","first-page":"1","volume":"31","author":"T.L. Gary","year":"2006","unstructured":"Gary, T.L., Albert, L.B., Clyde, R.: Preliminary Design of JML: A Behavioral Interface Specification Language for Java. SIGSOFT Softw. Eng. Notes\u00a031(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"10","key":"18_CR14","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"2","key":"18_CR15","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/MAHC.2003.1203056","volume":"25","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: Assertions: A Personal Perspective. IEEE Annals of the History of Comput-ing\u00a025(2), 14\u201325 (2003)","journal-title":"IEEE Annals of the History of Comput-ing"},{"issue":"2","key":"18_CR16","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MAHC.2003.1203057","volume":"25","author":"C.B. Jones","year":"2003","unstructured":"Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Annals of the History of Computing\u00a025(2), 26\u201349 (2003)","journal-title":"IEEE Annals of the History of Computing"},{"key":"18_CR17","doi-asserted-by":"crossref","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: Haim Kilov, B.R., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer, Dordrecht (1999)"},{"key":"18_CR18","unstructured":"Leavens, G.T., Cheon, Y.: Design by Contract with JML (2006), \n                    \n                      http:\/\/www.jmlspecs.org"},{"issue":"1-3","key":"18_CR19","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 ac-commodates both runtime assertion checking and formal verification. Science of Com-puter Programming\u00a055(1-3), 185\u2013208 (2005)","journal-title":"Science of Com-puter Programming"},{"key":"18_CR20","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual (2007), \n                    \n                      http:\/\/www.jmlspecs.org"},{"key":"18_CR21","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Prentice-Hall, Englewood Cliffs (1999)"},{"issue":"10","key":"18_CR22","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying Design by Contract. Computer\u00a025(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"18_CR23","unstructured":"Rioux, F.: Effective and Efficient Design by Contract for Java. M.Comp.Sc. thesis, Concordia University, Montr\u00e9al, Qu\u00e9bec (2006)"},{"issue":"3","key":"18_CR24","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/s10009-005-0218-5","volume":"8","author":"E. Robby","year":"2006","unstructured":"Robby, E., Rodr\u00edguez, M.B., Dwyer, M.B., Hatcliff, J.: Checking JML specifications using an extensible software model checking framework. International Journal on Software Tools for Technology Transfer (STTT)\u00a08(3), 280\u2013299 (2006)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"3","key":"18_CR25","first-page":"217","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM To-PLaS\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM To-PLaS"},{"key":"18_CR26","unstructured":"SAnToS, SpEx Website (2003), \n                    \n                      http:\/\/spex.projects.cis.ksu.edu"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:43:36Z","timestamp":1620017016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_18","relation":{},"subject":[]}}