{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:56:16Z","timestamp":1725566176356},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642156427"},{"type":"electronic","value":"9783642156434"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15643-4_21","type":"book-chapter","created":{"date-parts":[[2010,9,20]],"date-time":"2010-09-20T13:39:39Z","timestamp":1284989979000},"page":"276-290","source":"Crossref","is-referenced-by-count":2,"title":["Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems"],"prefix":"10.1007","author":[{"given":"Teng","family":"Long","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenhui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-78163-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Pnueli","year":"2008","unstructured":"Pnueli, A., Sa\u2019ar, Y.: All you need is compassion. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 233\u2013247. Springer, Heidelberg (2008)"},{"issue":"1","key":"21_CR2","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1142\/S0129054107004553","volume":"18","author":"I. Balaban","year":"2007","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Modular ranking abstraction. Int. J. Found. Comput. Sci.\u00a018(1), 5\u201344 (2007)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of c programs. In: PLDI, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"21_CR5","unstructured":"Long, T., Zhang, W.: Auxiliary constructs for proving liveness in compassion discrete systems. Technical Report, ISCAS\u2013LCS\u201309\u201303, Institute of Sofware, Chinese Academy of Sciences (2009), \n                    \n                      http:\/\/lcs.ios.ac.cn\/~zwh\/tr\/"},{"issue":"1","key":"21_CR6","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Inf. Comput.\u00a0163(1), 203\u2013243 (2000)","journal-title":"Inf. Comput."},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11562436_1","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Ranking abstraction as companion to predicate abstraction. In: Wang, F. (ed.) FORTE 2005. LNCS, vol.\u00a03731, pp. 1\u201312. Springer, Heidelberg (2005)"},{"issue":"4","key":"21_CR8","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1006\/jcss.2000.1744","volume":"62","author":"Y. Kesten","year":"2001","unstructured":"Kesten, Y., Pnueli, A., Vardi, M.Y.: Verification by augmented abstraction: The automata-theoretic view. J. Comput. Syst. Sci.\u00a062(4), 668\u2013690 (2001)","journal-title":"J. Comput. Syst. Sci."},{"key":"21_CR9","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.D.: Liveness with invisible ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 223\u2013238. Springer, Heidelberg (2004)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-540-24730-2_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Fang","year":"2004","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with incomprehensible ranking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 482\u2013496. Springer, Heidelberg (2004)"},{"issue":"1","key":"21_CR11","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci.\u00a083(1), 91\u2013130 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"21_CR12","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.L.: Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program.\u00a08(3), 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"21_CR13","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.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)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15643-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T00:19:32Z","timestamp":1553127572000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15643-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642156427","9783642156434"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15643-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}