{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:52Z","timestamp":1725490252198},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665878"},{"type":"electronic","value":"9783540481195"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48119-2_12","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T21:23:00Z","timestamp":1188336180000},"page":"173-194","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software"],"prefix":"10.1007","author":[{"given":"Yonit","family":"Kesten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amit","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gil","family":"Raanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Trans. Prog. Lang. Sys., 15:73\u2013132, 1993.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"issue":"3","key":"12_CR2","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. Prog. Lang. Sys., 17(3):507\u2013534, 1995.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"12_CR3","unstructured":"N. Bj\u00f8rner, I.A. Browne, E. Chang, M. Co\u00f3n, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover, User\u2019s Manual. Technical Report, Stanford University, 1995."},{"issue":"2","key":"12_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-15239-3","volume-title":"Proc. of Seminar on Concurrency","author":"H. Barringer","year":"1985","unstructured":"H. Barringer and R. Kuiper. Hierarchical development of concurrent systems in a temporal logic framework. In Proc. of Seminar on Concurrency, LNCS 197, 1985."},{"key":"12_CR6","unstructured":"P. Collete and A. Cau. Parallel composition of assumption-commitment specifications: A unifying approach for shared variables and distributed message passing concurrency. Acta Informatica, 1995."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking. In Model Checking, Abstraction and Composition, volume 152 of Nato ASI Series F, pages 477\u2013498. Springer-Verlag, 1996.","DOI":"10.1007\/978-3-642-61455-2_16"},{"issue":"4","key":"12_CR8","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"K.M. Chandy","year":"1981","unstructured":"K.M. Chandy and J. Misra. Proofs of networks of processes. IEEE Trans. Software Engin., 7(4):417\u2013426, 1981.","journal-title":"IEEE Trans. Software Engin."},{"key":"12_CR9","unstructured":"W.-P. de Roever. The quest for compositionality-a survey of assertion-based proof systems for concurrent programs, part i: Concurrency based on shared variables. In The Role of Abstract Models in Computer Science, pages 181\u2013206. IFIP, North Holland, 1985."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1984.","DOI":"10.1007\/978-3-662-09507-2_19"},{"key":"12_CR11","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, Engelwood Clis, NJ, 1991."},{"issue":"4","key":"12_CR12","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Trans. Prog. Lang. Sys., 5(4):596\u2013619, 1983.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"issue":"2","key":"12_CR13","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/174662.174665","volume":"16","author":"B. Jonsson","year":"1994","unstructured":"B. Jonsson. Compositional specification and verification of distributed systems. ACM Trans. Prog. Lang. Sys., 16(2):259\u2013303, 1994.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1995.1024","volume":"117","author":"R.P. Kurshan","year":"1995","unstructured":"R.P. Kurshan and K.L. McMillan. A structural induction theorem for processes. Information and Computation, 117:1\u201311, 1995.","journal-title":"Information and Computation"},{"key":"12_CR15","unstructured":"Y. Kesten and A. Pnueli. Deductive verification of fair discrete systems. Technical report, Weizmann Institute, 1998."},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. In ICALP\u201998 pages 1\u201316.","DOI":"10.1007\/BFb0055036"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Engin., 3:125\u2013143, 1977.","journal-title":"IEEE Trans. Software Engin."},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proc. 9th ACM Symp. Princ. of Dist. Comp., pages 377\u2013408, 1990.","DOI":"10.1145\/93385.93442"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"12_CR20","unstructured":"S. Owre, N. Shankar, and J.M. Rushby. User guide for the PVS specification and verification system. SRI International, Menlo Park, CA, 1993."},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BF02311231","volume":"5","author":"P.K. Pandya","year":"1991","unstructured":"P.K. Pandya and M. Joseph. P-A logic-a compositional proof system for distributed programs. Dist. Comp., 5:37\u201354, 1991.","journal-title":"Dist. Comp."},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, sub-series F: Computer and System Science, pages 123\u2013144. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"issue":"2","key":"12_CR23","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q.W. Xu","year":"1997","unstructured":"Q.W. Xu, W.-P. de Roever, and J.-F. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149\u2013174, 1997.","journal-title":"Formal Aspects of Computing"},{"key":"12_CR24","unstructured":"J. Zwiers. Compositionality Concurrency and Partial Correctness, volume 321 of Lect. Notes in Comp. Sci. Springer-Verlag, 1989."}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48119-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T19:09:23Z","timestamp":1684004963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48119-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665878","9783540481195"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-48119-2_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"17 September 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}