{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:42:58Z","timestamp":1742913778060,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44880-2_17","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"260-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Proving Temporal Properties of Z Specifications Using Abstraction"],"prefix":"10.1007","author":[{"given":"Graeme","family":"Smith","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kirsten","family":"Winter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis framework. In 6th ACM Symposium on Principles of Programming Languages, 1979.","DOI":"10.1145\/567752.567778"},{"key":"17_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification (CAV\u201900)","author":"E. Clarke","year":"2000","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In A.P. Sistla E.A. Emerson, editor, Computer Aided Verification (CAV\u201900), volume 1855 of LNCS. Springer-Verlag, 2000."},{"issue":"5","key":"17_CR3","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR4","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000."},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"J. Derrick and E. Boiten. Refinement in Z and Object-Z, Foundations and Advanced Applications. Springer-Verlag, 2001.","DOI":"10.1007\/978-1-4471-0257-1"},{"key":"17_CR6","unstructured":"P. Strooper D. Hazel and O. Traynor. Possum: An animator for the SUM specification language. In W. Wong and K. Leung, editors, Asia Pacific Software Engineering Conference (APSEC 97), pages 42\u201351. IEEE Computer Society, 1997."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 996\u20131072. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"17_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Int. Conf. on Computer Aided Verification (CAV 97)","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In Int. Conf. on Computer Aided Verification (CAV 97), volume 1254 of LNCS, pages 72\u201383. Springer-Verlag, 1997."},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/3-540-58555-9_113","volume-title":"Formal Methods Europe (FME\u201994)","author":"D. Jackson","year":"1994","unstructured":"D. Jackson. Abstract model checking of infinite specifications. In M. Naftalin, T. Denvir, and M. Bertran, editors, Formal Methods Europe (FME\u201994), volume 873 of LNCS, pages 519\u2013531. Springer-Verlag, 1994."},{"key":"17_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BFb0105411","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 96)","author":"Kolyang","year":"1996","unstructured":"Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle\/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics (TPHOLs 96), volume 1125 of LNCS, pages 283\u2013298. Springer-Verlag, 1996."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), 1995.","DOI":"10.1007\/BF01384313"},{"key":"17_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/3-540-45614-7_10","volume-title":"Formal Methods Europe FME\u20192002)","author":"A. Mota","year":"2002","unstructured":"A. Mota, P. Borba, and A. Sampaio. Mechanical abstraction of CSPZ processes. In L.-H. Eriksson and P. Lindsay, editors, Formal Methods Europe FME\u20192002), volume 2391 of LNCS, pages 163\u2013183. Springer-Verlag, 2002."},{"key":"17_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"International Conference of Z User (ZUM 97)","author":"M. Saaltink","year":"1997","unstructured":"M. Saaltink. The Z-Eves system. In J. Bowen, M. Hinchey, and D. Till, editors, International Conference of Z User (ZUM 97), volume 1212 of LNCS, pages 72\u201385. Springer-Verlag, 1997."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"G. Smith. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"17_CR15","unstructured":"J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 2nd edition, 1992."},{"key":"17_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification (CAV 99)","author":"H. Sa\u00efdi","year":"1999","unstructured":"H. Sa\u00efdi and N. Shankar. Abstract and model check while you prove. In N. Halbwachs and D. Peled, editors, Computer Aided Verification (CAV 99), volume 1633 of LNCS, pages 443\u2013454. Springer-Verlag, 1999."},{"issue":"3","key":"17_CR17","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1002\/spe.4380250306","volume":"25","author":"I. Toyn","year":"1995","unstructured":"I. Toyn and J. McDermid. CADiZ: An architecture for Z tools and its implementation. Software \u2014 Practice and Experience, 25(3):305\u2013330, 1995.","journal-title":"Software \u2014 Practice and Experience"},{"key":"17_CR18","series-title":"Lect Notes Comput Sci","volume-title":"World Congress on Formal Methods (FM\u201999)","author":"H. Wehrheim","year":"1999","unstructured":"H. Wehrheim. Data abstraction for CSP-OZ. In J. Woodcock and J. Wing, editors, World Congress on Formal Methods (FM\u201999), volume 1709 of LNCS. Springer-Verlag, 1999."},{"key":"17_CR19","series-title":"Lect Notes Comput Sci","volume-title":"3rd International Conference of Z and B Users (ZB 2003)","author":"K. Winter","year":"2003","unstructured":"K. Winter and G. Smith. Compositional verification for Object-Z. In 3rd International Conference of Z and B Users (ZB 2003), LNCS. Springer-Verlag, 2003. This volume."},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/S0167-6423(96)00020-2","volume":"28","author":"J. M. Wing","year":"1997","unstructured":"J. M. Wing and M. Vaziri-Farahani. A case study in model checking software systems. Science of Computer Programming, 28:273\u2013299, 1997.","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,23]],"date-time":"2023-01-23T20:27:55Z","timestamp":1674505675000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}