{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T07:44:54Z","timestamp":1767771894622},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540359074"},{"type":"electronic","value":"9783540359081"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11787006_45","type":"book-chapter","created":{"date-parts":[[2006,6,28]],"date-time":"2006-06-28T23:23:09Z","timestamp":1151536989000},"page":"528-539","source":"Crossref","is-referenced-by-count":11,"title":["Invisible Safety of Distributed Protocols"],"prefix":"10.1007","author":[{"given":"Ittai","family":"Balaban","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"45_CR1","unstructured":"Shankar, N., Owre, S., Rushby, J.M.: A tutorial on specification and verification using PVS. Technical report (1993)"},{"key":"45_CR2","unstructured":"Bj\u00f8rner, N., Browne, I., Chang, E., Col\u00f3n, M., Kapur, A., Manna, Z., Sipma, H., Uribe, T.: STeP: The Stanford Temporal Prover, User\u2019s Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University (1995)"},{"key":"45_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"45_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"45_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Arons, T., Ruah, S., Xu, J., Zuck, L.D.: Parameterized Verification with Automatically Computed Inductive Assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"45_CR6","doi-asserted-by":"crossref","unstructured":"Balaban, I., Fang, Y., Pnueli, A., Zuck, L.: IIV: An invisible invariant verifier. In: Computer Aided Verification (CAV) (2005)","DOI":"10.1007\/11513988_39"},{"issue":"3\u20134","key":"45_CR7","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.cl.2004.02.006","volume":"30","author":"L. Zuck","year":"2004","unstructured":"Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems. Computer Languages, Systems, and Structures\u00a030(3\u20134), 139\u2013169 (2004)","journal-title":"Computer Languages, Systems, and Structures"},{"key":"45_CR8","doi-asserted-by":"crossref","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized verification of a cache coherence protocol safety and liveness. In: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 317\u2013330 (2002)","DOI":"10.1007\/3-540-47813-2_22"},{"key":"45_CR9","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Bryant, R.: Constructing quantified invariants via predicate abstraction. In: Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 267\u2013281 (2004)","DOI":"10.1007\/978-3-540-24622-0_22"},{"key":"45_CR10","unstructured":"Romijn, J.M.T.: A timed verification of the IEEE 1394 leader election protocol. In: Gnesi, S., Latella, D. (eds.) Proceedings of the Fourth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS 1999), pp. 3\u201329 (1999)"},{"key":"45_CR11","unstructured":"Devillers, M., Griffioen, W., Romijn, J., Vaandrager, F.: Verification of a leader election protocol: Formal methods applied to IEEE 1394. Technical Report CSI-R9728, Computing Science Institute, Nijmegen (1997)"},{"key":"45_CR12","volume-title":"Proc. 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2002)","author":"C. Daws","year":"2002","unstructured":"Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. In: Cleaveland, R., Garavel, H. (eds.) Proc. 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2002). 2 of Electronic Notes in Theoretical Computer Science, vol.\u00a066, Elsevier, Amsterdam (2002)"},{"key":"45_CR13","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, S., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: CADE, pp. 99\u2013115 (2005)","DOI":"10.1007\/11532231_8"},{"key":"45_CR14","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms, CA, USA. Morgan Kaufmann Publishers, San Francisco (1996)"},{"key":"45_CR15","doi-asserted-by":"crossref","unstructured":"Balaban, I., Pnueli, A., Zuck, L.: Shape analysis by predicate abstraction. In: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 164\u2013180 (2005)","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"45_CR16","doi-asserted-by":"crossref","unstructured":"Balaban, I., Pnueli, A., Zuck, L.: Invisible safety of distributed protocols. Technical report, Computer Science Department, New York University (2006) http:\/\/www.cs.nyu.edu\/acsys\/pubs\/permanent\/distprotocolsicalp06full.pdf","DOI":"10.1007\/11787006_45"},{"issue":"4","key":"45_CR17","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1137\/0215074","volume":"15","author":"M. Luby","year":"1986","unstructured":"Luby, M.: A simple parallel algorithm for the maximal independent set problem. SIAM Journal of Computing\u00a015(4), 1036\u20131053 (1986)","journal-title":"SIAM Journal of Computing"},{"key":"45_CR18","unstructured":"Shahar, E.: The TLV Manual.(2000) http:\/\/www.cs.nyu.edu\/acsys\/tlv"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11787006_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:20:18Z","timestamp":1619508018000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11787006_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540359074","9783540359081"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11787006_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}