{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:05:06Z","timestamp":1725473106949},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540474609"},{"type":"electronic","value":"9783540474623"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11901433_37","type":"book-chapter","created":{"date-parts":[[2006,11,20]],"date-time":"2006-11-20T12:40:51Z","timestamp":1164026451000},"page":"678-696","source":"Crossref","is-referenced-by-count":14,"title":["Issues in Implementing 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":"Tony","family":"Simons","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"37_CR1","unstructured":"ISO\/IEC 13568:2002. Information technology\u2014Z formal specification notation\u2014syntax, type system and semantics. International Standard"},{"issue":"2","key":"37_CR2","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"},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"37_CR4","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"37_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":"37_CR6","first-page":"315","volume-title":"International Conference on Integrated Formal Methods (IFM 1999)","author":"C. Fischer","year":"1999","unstructured":"Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: Araki, K., Galloway, A., Taguchi, K. (eds.) International Conference on Integrated Formal Methods (IFM 1999), pp. 315\u2013334. Springer, Heidelberg (1999)"},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"37_CR8","volume-title":"Asia-Pacific Software Engineering Conference (APSEC 2001)","author":"G. Kassel","year":"2001","unstructured":"Kassel, G., Smith, G.: Model checking Object-Z classes: Some experiments with FDR. In: Asia-Pacific Software Engineering Conference (APSEC 2001). IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"37_CR9","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":"37_CR10","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.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol.\u00a03771, pp. 227\u2013245. Springer, Heidelberg (2005)"},{"key":"37_CR11","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0167-6423(00)00023-X","volume":"40","author":"A. Mota","year":"2001","unstructured":"Mota, A., Sampaio, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming\u00a040, 59\u201396 (2001)","journal-title":"Science of Computer Programming"},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"37_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.C., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, pp. 85\u2013103. Springer, Heidelberg (2005)"},{"key":"37_CR14","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"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901433_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:01:10Z","timestamp":1558288870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901433_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540474609","9783540474623"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/11901433_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}