{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:49:29Z","timestamp":1725504569320},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540781622"},{"type":"electronic","value":"9783540781639"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_21","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T10:30:06Z","timestamp":1204281006000},"page":"233-247","source":"Crossref","is-referenced-by-count":15,"title":["All You Need Is Compassion"],"prefix":"10.1007","author":[{"given":"Amir","family":"Pnueli","sequence":"first","affiliation":[]},{"given":"Yaniv","family":"Sa\u2019ar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"21_CR1","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_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/3-540-60692-0_69","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"I. Browne","year":"1995","unstructured":"Browne, I., Manna, Z., Sipma, H.: Generalized verification diagrams. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 484\u2013498. Springer, Heidelberg (1995)"},{"key":"21_CR4","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"21_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":"21_CR6","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: Proc. 34th ACM Symp. Princ. of Prog. Lang., pp. 265\u2013276 (2007)","DOI":"10.1145\/1190216.1190257"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"21_CR8","unstructured":"Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Gopalakrishnan, G. (ed.) Workshop on Advances in Verification, pp. 1\u20138 (2000)"},{"issue":"1","key":"21_CR9","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.ic.2005.01.006","volume":"200","author":"Y. Kesten","year":"2005","unstructured":"Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. Inf. and Comp.\u00a0200(1), 35\u201361 (2005)","journal-title":"Inf. and Comp."},{"issue":"1","key":"21_CR10","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by finitary abstraction. Information and Computation, a special issue on Compositionality\u00a0163(1), 203\u2013243 (2000)","journal-title":"Information and Computation, a special issue on Compositionality"},{"issue":"2\u20133","key":"21_CR11","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.tcs.2004.09.023","volume":"331","author":"Y. Kesten","year":"2005","unstructured":"Kesten, Y., Pnueli, A.: A Compositional Approach to CTL* Verification. Theor. Comp. Sci.\u00a0331(2\u20133), 397\u2013428 (2005)","journal-title":"Theor. Comp. Sci."},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45694-5_8","volume-title":"CONCUR 2002 - Concurrency Theory","author":"Y. Kesten","year":"2002","unstructured":"Kesten, Y., et al.: Network invariants in action. In: Brim, L., et al. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 101\u2013115. Springer, Heidelberg (2002)"},{"key":"21_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. Trans. Soft. Eng.\u00a03, 125\u2013143 (1977)","journal-title":"Trans. Soft. Eng."},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Manna, Z., et al.: STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California (1994)","DOI":"10.21236\/ADA324036"},{"issue":"1","key":"21_CR15","doi-asserted-by":"publisher","first-page":"97","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. Comp. Sci.\u00a083(1), 97\u2013130 (1991)","journal-title":"Theor. Comp. Sci."},{"key":"21_CR16","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":"21_CR17","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Progress. Draft manuscript (1996), http:\/\/theory.stanford.edu\/~zm\/tvors3.html","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"21_CR18","volume-title":"PVS System Guide","author":"S. Owre","year":"2001","unstructured":"Owre, S., et al.: PVS System Guide. Menlo Park, CA (2001)"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","first-page":"598","volume-title":"Verification: Theory and Practice","author":"A. Pnueli","year":"2004","unstructured":"Pnueli, A., Arons, T.: TLPVS: A PVS-Based LTL Verification System. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 598\u2013625. Springer, Heidelberg (2004)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/978-3-540-31980-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2005","unstructured":"Pnueli, A., Podelski, A., Rybalchenko, A.: Separating fairness and well-foundedness for the analysis of fair discrete systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 124\u2013139. Springer, Heidelberg (2005)"},{"key":"21_CR21","unstructured":"Pnueli, A., Sa\u2019ar, Y.: All you need is compassion. Research Report, Dept. of Computer Science, New York University Technical Report (October 2007), http:\/\/www.cs.nyu.edu\/acsys\/pubs\/permanent\/all-you-need-is-compassion.pdf"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL 2005, pp. 132\u2013144 (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"1","key":"21_CR25","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1023\/A:1008791913551","volume":"15","author":"H.B. Sipma","year":"1999","unstructured":"Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. Formal Methods in System Design\u00a015(1), 49\u201374 (1999)","journal-title":"Formal Methods in System Design"},{"key":"21_CR26","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1016\/0890-5401(89)90004-7","volume":"82","author":"F.A. Stomp","year":"1989","unstructured":"Stomp, F.A., de Roever, W.-P., Gerth, R.T.: The \u03bc-calculus as an assertion language for fairness arguments. Inf. and Comp.\u00a082, 278\u2013322 (1989)","journal-title":"Inf. and Comp."},{"key":"21_CR27","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS 1986, pp. 332\u2013344 (1986)"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 68\u201380. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78163-9_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:13:29Z","timestamp":1606184009000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_21","relation":{},"subject":[]}}