{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:37Z","timestamp":1761611137664},"reference-count":41,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3650,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1016\/s1571-0661(04)80810-7","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"75-91","source":"Crossref","is-referenced-by-count":38,"special_numbering":"C","title":["An overview of JML tools and applications1 1www.jmlspecs.org"],"prefix":"10.1016","volume":"80","author":[{"given":"Lilian","family":"Burdy","sequence":"first","affiliation":[]},{"given":"Yoonsik","family":"Cheon","sequence":"additional","affiliation":[]},{"given":"David","family":"Cok","sequence":"additional","affiliation":[]},{"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[]},{"given":"Joe","family":"Kiniry","sequence":"additional","affiliation":[]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[]},{"given":"K.","family":"Rustan","sequence":"additional","affiliation":[]},{"given":"M.","family":"Leino","sequence":"additional","affiliation":[]},{"given":"Erik","family":"Poll","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB1","series-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"issue":"1","key":"10.1016\/S1571-0661(04)80810-7_NEWBIB2","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1109\/32.825766","article-title":"Automatically checking an implementation against its formal specification","volume":"26","author":"Antoy","year":"2000","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB3","doi-asserted-by":"crossref","unstructured":"D. Bartetzko, C. Fischer, M. Moller, and H. Wehrheim. Jass \u2013- Java with assertions. In Workshop on Runtime Verification at CAV '01, 2001. Published in ENTCS, K. Havelund and G. Rosu (eds.), 55(2), 2001.","DOI":"10.1016\/S1571-0661(04)00247-6"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB4","unstructured":"Kent Beck and Erich Gamma. Test infected: Programmers love writing tests. Java Report, 3(7):37\u201350, 1998."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB5","series-title":"AMAST'02, number 2422 in LNCS","first-page":"304","article-title":"Specifying and verifying a decimal representation in Java for smart cards","author":"Breunesse","year":"2002"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB6","series-title":"TPHOL '02","first-page":"99","article-title":"A proposal for a formal OCL semantics in Isabelle\/HOL","author":"Achim Brucker","year":"2002"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB7","unstructured":"Lilian Burdy, Jean-Louis Lanet, and Antoine Requet. JACK (Java Applet Correctness Kit). At http:\/\/www.gemplus.com\/smart\/r_d\/trends\/jack.html, 2002."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB8","series-title":"FME 2002","first-page":"272","article-title":"Formal specification of Gemplus's electronic purse case study","author":"Cata\u00f1o","year":"2002"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB9","series-title":"VMCAI: Verification, Model Checking, and Abstract Interpretation","first-page":"26","article-title":"CHASE: A static checker for JML's assignable clause","author":"Cata&nTo","year":"2003"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB10","unstructured":"Yoonsik Cheon and Gary T. Leavens. A runtime assertion checker for the Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun, editors, the International Conference on Software Engineering Research and Practice (SERP '02), pages 322\u2013328. CSREA Press, June 2002."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB11","series-title":"ECOOP 2002","first-page":"231","article-title":"A simple and practical approach to unit testing: The JML and JUnit way","author":"Cheon","year":"2002"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB12","unstructured":"Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, and Stephen Edwards. Model variables: Cleanly supporting abstraction in design by contract. Technical Report 03\u201310, Department of Computer Science, Iowa State University, April 2003. Available from archives.cs.iastate.edu."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB13","doi-asserted-by":"crossref","unstructured":"Krishna Kishore Dhara and Gary T. Leavens. Forcing behavioral subtyping through specification inheritance. In 18th International Conference on Software Engineering, pages 258\u2013267. IEEE Computer Society Press, 1996.","DOI":"10.1109\/ICSE.1996.493421"},{"issue":"2","key":"10.1016\/S1571-0661(04)80810-7_NEWBIB14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/32.908957","article-title":"Dynamically discovering likely program invariants to support program evolution","volume":"27","author":"Ernst","year":"2001","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB15","doi-asserted-by":"crossref","unstructured":"Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin. Quickly detecting relevant program invariants. In ICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, pages 449\u2013458, 2000.","DOI":"10.1109\/ICSE.2000.870435"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB16","series-title":"FME 2001","first-page":"500","article-title":"Houdini, an annotation assistant for esc\/java","author":"Flanagan","year":"2001"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB17","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'2002), pages 234\u2013245, 2002.","DOI":"10.1145\/543552.512558"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB18","series-title":"IWHD'95","first-page":"151","article-title":"The design of distributed hyperlinked programming documentation","author":"Friendly","year":"1995"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB19","series-title":"Larch: Languages and Tools for Formal Specification","author":"Guttag","year":"1993"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB20","unstructured":"Marieke Huisman. Reasoning about Java Programs in higher order logic with PVS and Isabelle. IPA dissertation series, 2001\u201303, University of Nijmegen, Holland, February 2001."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB21","unstructured":"Bart Jacobs. Weakest precondition reasoning for Java programs with JML annotations. JLAP, 2002. To appear."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB22","series-title":"Fundamental Approaches to Software Engineering (FASE)","first-page":"284","article-title":"A logic for the Java Modeling Language JML","author":"Jacobs","year":"2001"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB23","doi-asserted-by":"crossref","unstructured":"Bart Jacobs, Joachim van den Berg, Marieke Huisman, Martijn van Berkum, Ulrich Hensel, and Hendrik Tews. Reasoning about Java classes (preliminary report). In OOPSLA'98, volume 33(10) of ACM SIGPLAN Notices, pages 329\u2013340. ACM, October 1998.","DOI":"10.1145\/286936.286973"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB24","series-title":"TOOLS 26: Technology of Object-Oriented Languages and Systems, Los Alamitos, California","first-page":"295","article-title":"iContract - the Java design by contract tool","author":"Kramer","year":"1998"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB25","series-title":"Behavioral Specifications of Businesses and Systems","first-page":"175","article-title":"JML: A notation for detailed design","author":"Leavens","year":"1999"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB26","unstructured":"Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98\u201306u, Iowa State University, Department of Computer Science, April 2003. See www.jmlspecs.org."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB27","doi-asserted-by":"crossref","unstructured":"Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Technical Report 03\u201304, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, March 2003. To appear in the proceedings of FMCO 2002.","DOI":"10.1007\/978-3-540-39656-7_11"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB28","unstructured":"K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC\/Java user's manual. Technical Note 2000\u2013002, Compaq SRC, October 2000."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB29","unstructured":"K. Rustan M. Leino, James B. Saxe, and Raymie Stata. Checking Java programs via guarded commands. Technical Note 1999\u2013002, Compaq SRC, May 1999."},{"issue":"6","key":"10.1016\/S1571-0661(04)80810-7_NEWBIB30","doi-asserted-by":"crossref","first-page":"1811","DOI":"10.1145\/197320.197383","article-title":"A behavioral notion of subtyping","volume":"16","author":"Liskov","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB31","unstructured":"Claude March\u00e9, Christine Paulin, and Xavier Urbain. The Krakatoa tool for JML\/Java program certification. Available at http:\/\/krakatoa.lri.fr, 2003."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB32","unstructured":"Renaud Marlet and Daniel Le Metayer. Security properties and Java Card specificities to be studied in the SecSafe project. Technical Report SECSAFETL-006, Trusted Logic, August 2001. Available from http:\/\/www.doc.ic.ac.uk\/~siveroni\/secsafe\/docs.html."},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB33","series-title":"Object-oriented Software Construction","author":"Meyer","year":"1997"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB34","doi-asserted-by":"crossref","unstructured":"Jeremy W. Nimmer and Michael D. Ernst. Automatic generation of program specifications. In ISSTA 2002, International Symposium on Software Testing and Analysis, pages 232\u2013242, Rome, Italy, 2002.","DOI":"10.1145\/566210.566213"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB35","doi-asserted-by":"crossref","unstructured":"Jeremy W. Nimmer and Michael D. Ernst. Invariant inference for static checking: An empirical evaluation. In ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering (FSE 2002), pages 11\u201320, 2002.","DOI":"10.1145\/605466.605469"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB36","series-title":"Computer Aided Verification","first-page":"411","article-title":"PVS: Combining specification, proof checking, and model checking","author":"Owre","year":"1996"},{"issue":"3","key":"10.1016\/S1571-0661(04)80810-7_NEWBIB37","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1109\/32.667877","article-title":"Using test oracles generated from program documentation","volume":"24","author":"Peters","year":"1998","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB38","unstructured":"Erik Poll, Pieter Hartel, and Eduard de Jong. A Java reference model of transacted memory for smart cards. In Smart Card Research and Advanced Application Conference (CARDIS'2002), pages 75\u201386. USENIX, 2002."},{"issue":"4","key":"10.1016\/S1571-0661(04)80810-7_NEWBIB39","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1016\/S1389-1286(01)00163-3","article-title":"Formal specification of the Java Card API in JML: the APDU class","volume":"36","author":"Poll","year":"2001","journal-title":"Computer Networks"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB40","series-title":"The Unified Modeling Language Reference Manual","author":"Rumbaugh","year":"1998"},{"key":"10.1016\/S1571-0661(04)80810-7_NEWBIB41","series-title":"The Object Constraint Language: Precise Modeling with UML","author":"Warmer","year":"1999"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104808107?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104808107?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:13:29Z","timestamp":1585898009000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104808107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":41,"alternative-id":["S1571066104808107"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80810-7","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}