{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:32:48Z","timestamp":1725492768893},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441571"},{"type":"electronic","value":"9783540457329"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45732-1_13","type":"book-chapter","created":{"date-parts":[[2007,10,11]],"date-time":"2007-10-11T00:38:56Z","timestamp":1192063136000},"page":"113-125","source":"Crossref","is-referenced-by-count":1,"title":["A Strategy for Improving the Efficiency of Procedure Verification"],"prefix":"10.1007","author":[{"given":"Wenhui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/3-540-49213-5_4","volume-title":"Proceedings of COMPOS\u201997","author":"S. Berezin","year":"1998","unstructured":"S. Berezin and S. Campos and E. M. Clarke. Compositional Reasoning in Model Checking. Proceedings of COMPOS\u201997. Lecture Notes in Computer Science 1536: 81\u2013102. 1998."},{"issue":"5","key":"13_CR2","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg and D.E. 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":"13_CR3","first-page":"997","volume":"B","author":"E.A. Emerson","year":"1990","unstructured":"E.A. Emerson. Temporal and Modal Logic. Handbook of Theoretical Computer Science (B):997\u20131072. 1990.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"13_CR4","first-page":"280","volume":"VII","author":"J. Gregoire","year":"1995","unstructured":"J. Gregoire. Verification Model Reduction through Abstraction. Formal Design Techniques VII, 280\u2013282, 1995.","journal-title":"Formal Design Techniques"},{"key":"13_CR5","volume-title":"Design and Validation of Computer Protocols","author":"G. J. Holzmann","year":"1991","unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, New Jersey, 1991."},{"issue":"5","key":"13_CR6","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering 23(5): 279\u2013295. May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR7","unstructured":"J.G. Kemeny. Report of the President\u2019s Commission on the Accident at Three Mile Island. U. S. Government Accounting Office. 1979."},{"key":"13_CR8","unstructured":"N.G. Leveson. Software System Safety and Computers. Addison-Wesley Publishing Company. 1995."},{"key":"13_CR9","first-page":"1","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Journal of Formal methods in System Design 6:1\u201335. 1995.","journal-title":"Journal of Formal methods in System Design"},{"key":"13_CR10","first-page":"235","volume":"3","author":"V. Roy","year":"1990","unstructured":"V. Roy and R. de Simone. Auto\/Autograph. In Computer Aided Verification. DIMACS series in Discrete Mathematics and Theoretical Computer Science 3: 235\u2013250, June 1990.","journal-title":"DIMACS series in Discrete Mathematics and Theoretical Computer Science"},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-48234-2_16","volume-title":"Model checking operator procedures","author":"W. Zhang","year":"1999","unstructured":"W. Zhang. Model checking operator procedures. Lecture Notes in Computer Science 1680:200\u2013215. SPIN 1999. Toulouse, France."},{"key":"13_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-40891-6_5","volume-title":"Validation of control system specifications with abstract plant models","author":"W. Zhang","year":"2000","unstructured":"W. Zhang. Validation of control system specifications with abstract plant models. Lecture Notes in Computer Science 1943:53\u201362. SAFECOMP 2000. Rotterdam, The Netherlands."}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45732-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T05:05:56Z","timestamp":1550984756000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45732-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441571","9783540457329"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45732-1_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}