{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:45:13Z","timestamp":1743065113990,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466803"},{"type":"electronic","value":"9783662466810"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_30","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:56:36Z","timestamp":1427741796000},"page":"384-398","source":"Crossref","is-referenced-by-count":11,"title":["Fairness for Infinite-State Systems"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Heidy","family":"Khlaaf","sequence":"additional","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Apt, K., Olderog, E.: Fairness in parallel programs: The transformational approach. In: ACM TOPLAS, vol.\u00a010 (1988)","DOI":"10.1145\/44501.44504"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"T.A. Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Browne, A., Col\u00f3n, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.: Verifying temporal properties of reactive systems: A step tutorial. FMSD 16(3) (2000)","DOI":"10.1023\/A:1008700623084"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M. Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 413\u2013429. Springer, Heidelberg (2013)"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 359. Springer, Heidelberg (2002)"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS 8(2) (1986)","DOI":"10.1145\/5397.5399"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Parkinson, M., Vafeiadis, V.: Proving that non-blocking algorithms don\u2019t block. In: POPL. ACM (2009)","DOI":"10.1145\/1594834.1480886"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.: Proving that programs eventually do something good. In: POPL. ACM (2007)","DOI":"10.1145\/1190216.1190257"},{"key":"30_CR9","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: Fairness for infinite-state systems. TR RN\/14\/11, UCL (2014)"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-45220-1_46","volume-title":"Computer Science Logic","author":"T. Rybina","year":"2003","unstructured":"Rybina, T., Voronkov, A.: Faster temporal reasoning for infinite-state programs. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol.\u00a02803, pp. 546\u2013573. Springer, Heidelberg (2003)"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: POPL. ACM (2011)","DOI":"10.1145\/1926385.1926431"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Cook, B., Koskinen, E.: Reasoning about nondeterminism in programs. In: PLDI. ACM (2013)","DOI":"10.1145\/2491956.2491969"},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-22110-1_26","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2011","unstructured":"Cook, B., Koskinen, E., Vardi, M.: Temporal property verification as a program analysis task. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 333\u2013348. Springer, Heidelberg (2011)"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 47\u201361. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11867340_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A. David","year":"2006","unstructured":"David, A., H\u00e5kansson, J., Larsen, K.G., Pettersson, P.: Model checking timed automata with priorities using DBM subtraction. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 128\u2013142. Springer, Heidelberg (2006)"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. J. ACM\u00a033(1) (January 1986)","DOI":"10.1145\/4904.4999"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-16078-7_62","volume-title":"STACS 86","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Lei, C.-L.: Temporal reasoning under generalized fairness constraints. In: Monien, B., Vidal-Naquet, G. (eds.) STACS 1986. LNCS, vol.\u00a0210, pp. 21\u201336. Springer, Heidelberg (1985)"},{"key":"30_CR18","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1145\/4904.4993","volume":"33","author":"D. Harel","year":"1986","unstructured":"Harel, D.: Effective transformations on infinite trees, with applications to high undecidability, dominoes and fairness. J. ACM\u00a033, 224\u2013248 (1986)","journal-title":"J. ACM"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"30_CR21","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)"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"30_CR23","unstructured":"Schwoon, S.: Moped - A Model-Checker for Pushdown Systems (2002), \n                      \n                        http:\/\/www7.in.tum.de\/~schwoon\/moped"},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: Pushdown model checking for malware detection. In: ESEC\/FSE (2013)","DOI":"10.1145\/2491411.2494599"},{"issue":"1","key":"30_CR25","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C\u00a0115(1), 1\u201337 (1994)","journal-title":"I&C"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:35:07Z","timestamp":1559140507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}