{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:45:00Z","timestamp":1725561900844},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212997"},{"type":"electronic","value":"9783540247302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_36","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T11:00:15Z","timestamp":1280746815000},"page":"482-496","source":"Crossref","is-referenced-by-count":13,"title":["Liveness with Incomprehensible Ranking"],"prefix":"10.1007","author":[{"given":"Yi","family":"Fang","sequence":"first","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic program verification of finite-state concurrent systems. IPL\u00a022(6) (1986)","key":"36_CR1","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"36_CR2","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":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 221. Springer, Heidelberg (2001)"},{"unstructured":"Bj\u00f8rner, N., Browne, I.A., Chang, E., Col\u00f3n, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: The Stanford Temporal Prover, User\u2019s Manual. Technical Report STAN-CS-TR-95-1562, CS Department, Stanford University (November 1995)","key":"36_CR3"},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-60218-6_30","volume-title":"CONCUR \u201995 Concurrency Theory","author":"E.M. Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parametrized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 395\u2013407. Springer, Heidelberg (1995)"},{"key":"36_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M. Colon","year":"2002","unstructured":"Colon, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"key":"36_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E.A. Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 236\u2013255. Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: 22nd POPL (1995)","key":"36_CR7","DOI":"10.1145\/199448.199468"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-24622-0_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Fang","year":"2004","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with invisible ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 223\u2013238. Springer, Heidelberg (2004)"},{"unstructured":"Gyuris, V., Sistla, A.P.: On-the-fly model checking under fairness that exploits symmetry. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 424\u2013438. Springer, Heidelberg (1998)","key":"36_CR9"},{"key":"36_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"E.P. Gribomont","year":"1997","unstructured":"Gribomont, E.P., Zenner, G.: Automated verification of szymanski\u2019s algorithm. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"36_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-46419-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Jonsson","year":"2000","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 220. Springer, Heidelberg (2000)"},{"key":"36_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-540-45069-6_36","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"2003","unstructured":"Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 381\u2013392. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: 24th POPL (1997)","key":"36_CR13","DOI":"10.1145\/263699.263747"},{"key":"36_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 110\u2013121. Springer, Heidelberg (1998)"},{"doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety (1995)","key":"36_CR15","DOI":"10.1007\/978-1-4612-4222-2"},{"unstructured":"Owre, S., Shankar, N., Rushby, J.M.: User guide for the PVS specification and verification system (draft). Tech. report, CS Lab., SRI International, CA (1993)","key":"36_CR16"},{"key":"36_CR17","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.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"36_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1,\u221e)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"unstructured":"Shahar, E.: The TLV Manual (2000), http:\/\/www.wisdom.weizmann.ac.il\/~verify\/tlv","key":"36_CR19"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24730-2_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T23:18:10Z","timestamp":1559344690000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}