{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T05:17:47Z","timestamp":1740287867219,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540278825"},{"type":"electronic","value":"9783540317142"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11526841_7","type":"book-chapter","created":{"date-parts":[[2010,7,18]],"date-time":"2010-07-18T16:51:58Z","timestamp":1279471918000},"page":"75-90","source":"Crossref","is-referenced-by-count":13,"title":["Symbolic Animation of JML Specifications"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Bouquet","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Dadeau","sequence":"additional","affiliation":[]},{"given":"Bruno","family":"Legeard","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Utting","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","first-page":"105","volume-title":"CONCUR 2002 - Concurrency Theory","author":"F. Ambert","year":"2002","unstructured":"Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Vacelet, N., Utting, M.: BZ-TT: A Tool-Set for Test Generation from Z and B using Contraint Logic Programming. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 105\u2013120. Springer, Heidelberg (2002)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","first-page":"435","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"F. Bouquet","year":"2005","unstructured":"Bouquet, F., Dadeau, F., Groslambert, J.: Checking JML Specifications with B Machines. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, pp. 435\u2013454. Springer, Heidelberg (2005)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-540-31980-1_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Bouquet","year":"2005","unstructured":"Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 551\u2013556. Springer, Heidelberg (2005)"},{"key":"7_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":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/3-540-36087-5_27","volume-title":"EurAsia-ICT 2002: Information and Communication Technology","author":"M. Gogolla","year":"2002","unstructured":"Gogolla, M., Richters, M.: Development of UML Descriptions with USE. In: Shafazand, H., Tjoa, A.M. (eds.) EurAsia-ICT 2002. LNCS, vol.\u00a02510, pp. 228\u2013238. Springer, Heidelberg (2002)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Gray, J., Schach, S.: Constraint Animation Using an Object-Oriented Declarative Language. In: Proceedings of the 38th Annual ACM SE Conference, Clemson (April 2000)","DOI":"10.1145\/1127716.1127718"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Hazel, D., Strooper, P., Traynor, O.: Possum: An Animator for the SUM Specification Language. In: Proceedings of the Fourth Asia-Pacific Software Engineering and International Computer Science Conference, pp. 42\u201351 (1997)","DOI":"10.1109\/APSEC.1997.640160"},{"key":"7_CR9","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java Modeling Language. In: Formal Underpinnings of Java Workshop (at OOPSLA 1998) (October 1998)"},{"issue":"2","key":"7_CR10","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1002\/stvr.287","volume":"14","author":"Bruno Legeard","year":"2004","unstructured":"Legeard, B., Peureux, F., Utting, M.: Controlling Test Case Explosion in Test Generation from B Formal Models. The Journal of Software Testing, Verification and Reliability\u00a014(2) (2004) (To appear)","journal-title":"Software Testing, Verification and Reliability"},{"key":"7_CR11","volume-title":"International conference on Software Engineering and Formal Methods (SEFM 2003)","author":"T. McComb","year":"2003","unstructured":"McComb, T., Smith, G.: Animation of Object-Z Specifications Using a Z Animator. In: International conference on Software Engineering and Formal Methods (SEFM 2003). IEEE\u00a0Computer Society, Los Alamitos (2003)"},{"key":"7_CR12","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"7_CR13","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.B., 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":"7_CR14","volume-title":"The Unified Modeling Language Reference Manual","author":"J. Rumbaugh","year":"1999","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-wesley, Reading (1999)"},{"key":"7_CR15","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)","edition":"2"},{"issue":"4","key":"7_CR16","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026554217992","volume":"7","author":"T. Wahls","year":"2000","unstructured":"Wahls, T., Leavens, G.T., Baker, A.L.: Executing Formal Specifications with Concurrent Constraint Programming. Automated Software Engineering\u00a07(4), 315\u2013343 (2000)","journal-title":"Automated Software Engineering"},{"key":"7_CR17","volume-title":"The Object Constraint Language: Precise Modeling with UML","author":"J. Warmer","year":"1988","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Reading (1988)"}],"container-title":["Lecture Notes in Computer Science","FM 2005: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11526841_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T02:30:29Z","timestamp":1740277829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11526841_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278825","9783540317142"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11526841_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}