{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:44:49Z","timestamp":1725518689404},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540876021"},{"type":"electronic","value":"9783540876038"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87603-8_22","type":"book-chapter","created":{"date-parts":[[2008,9,20]],"date-time":"2008-09-20T07:56:24Z","timestamp":1221897384000},"page":"280-293","source":"Crossref","is-referenced-by-count":10,"title":["Z2SAL - Building a Model Checker for Z"],"prefix":"10.1007","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[]},{"given":"Siobh\u00e1n","family":"North","sequence":"additional","affiliation":[]},{"given":"Anthony J. H.","family":"Simons","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"22_CR1","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.entcs.2005.04.023","volume":"137","author":"C. Bolton","year":"2005","unstructured":"Bolton, C.: Using the Alloy Analyzer to Verify Data Refinement in Z. Electronic Notes in Theoretical Computer Science\u00a0137(2), 23\u201344 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"8","key":"22_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"issue":"3","key":"22_CR3","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv.\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"key":"22_CR4","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"de Moura, L., Owre, S., Shankar, N.: The SAL language manual. Technical Report SRI-CSL-01-02 (Rev.2), SRI International (2003)","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"678","DOI":"10.1007\/11901433_37","volume-title":"Formal Methods and Software Engineering","author":"J. Derrick","year":"2006","unstructured":"Derrick, J., North, S., Simons, T.: Issues in implementing a model checker for z. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 678\u2013696. Springer, Heidelberg (2006)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/11576280_24","volume-title":"Formal Methods and Software Engineering","author":"M. Leuschel","year":"2005","unstructured":"Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 345\u2013359. Springer, Heidelberg (2005)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/11589976_14","volume-title":"Integrated Formal Methods","author":"T. Miller","year":"2005","unstructured":"Miller, T., Freitas, L., Malik, P., Utting, M.: CZT Support for Z Extensions. In: Romijn, J., Smith, G., Pol, J. (eds.) IFM 2005. LNCS, vol.\u00a03771, pp. 227\u2013245. Springer, Heidelberg (2005)"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D. Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z Specifications using the ProB Animator and Model Checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 480\u2013500. Springer, Heidelberg (2007)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/11415787_6","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"G. Smith","year":"2005","unstructured":"Smith, G., Wildman, L.: Model checking Z specifications using SAL. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, pp. 85\u2013103. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, B and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87603-8_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:05:10Z","timestamp":1606183510000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87603-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540876021","9783540876038"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87603-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}