{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T14:17:14Z","timestamp":1726409834055},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_9","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"123-139","source":"Crossref","is-referenced-by-count":15,"title":["Fair Model Checking with Process Counter Abstraction"],"prefix":"10.1007","author":[{"given":"Jun","family":"Sun","sequence":"first","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Abhik","family":"Roychoudhury","sequence":"additional","affiliation":[]},{"given":"Shanshan","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Agesen, O., Detlefs, D., Garthwaite, A., Knippel, R., Ramakrishna, Y.S., White, D.: An Efficient Meta-Lock for Implementing Ubiquitous Synchronization. In: OOPSLA, pp. 207\u2013222 (1999)","DOI":"10.1145\/320384.320402"},{"issue":"6","key":"9_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett.\u00a022(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"9_CR3","doi-asserted-by":"crossref","DOI":"10.1002\/0471478210","volume-title":"Distributed Computing: Fundamentals, Simulations, and Advanced Topics","author":"H. Attiya","year":"2004","unstructured":"Attiya, H., Welch, J.: Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd edn. John Wiley & Sons, Inc., Publication, Chichester (2004)","edition":"2"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-540-24732-6_15","volume-title":"Model Checking Software","author":"D. Bosnacki","year":"2004","unstructured":"Bosnacki, D., Ioustinova, N., Sidorova, N.: Using Fairness to Make Abstractions Work. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 198\u2013215. Springer, Heidelberg (2004)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/3-540-56922-7_37","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"1993","unstructured":"Clarke, E.M., Filkorn, T., Jha, S.: Exploiting Symmetry In Temporal Logic Model Checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 450\u2013462. Springer, Heidelberg (1993)"},{"key":"9_CR6","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Fair Model Checking of Abstractions. In: VCL 2000 (2000)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic Verification of Parameterized Cache Coherence Protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"issue":"4","key":"9_CR8","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On Reasoning About Rings. Int. J. Found. Comput. Sci.\u00a014(4), 527\u2013550 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"4","key":"9_CR9","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1145\/262004.262008","volume":"19","author":"E.A. Emerson","year":"1997","unstructured":"Emerson, E.A., Sistla, A.P.: Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach. ACM Trans. Program. Lang. Syst.\u00a019(4), 617\u2013638 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/11888116_26","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"Y. Fang","year":"2006","unstructured":"Fang, Y., McMillan, K.L., Pnueli, A., Zuck, L.D.: Liveness by Invisible Invariants. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol.\u00a04229, pp. 356\u2013371. Springer, Heidelberg (2006)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/11945529_28","volume-title":"Principles of Distributed Systems","author":"M.J. Fischer","year":"2006","unstructured":"Fischer, M.J., Jiang, H.: Self-stabilizing Leader Election in Networks of Finite-state Anonymous Agents. In: Shvartsman, M.M.A.A. (ed.) OPODIS 2006. LNCS, vol.\u00a04305, pp. 395\u2013409. Springer, Heidelberg (2006)"},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.tcs.2005.07.004","volume":"345","author":"J. Geldenhuys","year":"2005","unstructured":"Geldenhuys, J., Valmari, A.: More efficient on-the-fly LTL verification with Tarjan\u2019s algorithm. Theoretical Computer Science\u00a0345(1), 60\u201382 (2005)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about Systems with Many Processes. J. ACM\u00a039(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-63166-6_24","volume-title":"Computer Aided Verification","author":"V. Gyuris","year":"1997","unstructured":"Gyuris, V., Sistla, A.P.: On-the-Fly Model Checking Under Fairness That Exploits Symmetry. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 232\u2013243. Springer, Heidelberg (1997)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-540-31980-1_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Hammer","year":"2005","unstructured":"Hammer, M., Knapp, A., Merz, S.: Truly On-the-Fly LTL Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 191\u2013205. Springer, Heidelberg (2005)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/3-540-61422-2_117","volume-title":"Algorithm Theory - SWAT \u201996","author":"M.R. Henzinger","year":"1996","unstructured":"Henzinger, M.R., Telle, J.A.: Faster Algorithms for the Nonemptiness of Streett Automata and for Communication Protocol Pruning. In: Karlsson, R., Lingas, A. (eds.) SWAT 1996. LNCS, vol.\u00a01097, pp. 16\u201327. Springer, Heidelberg (1996)"},{"key":"9_CR17","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley, Reading (2003)"},{"issue":"3","key":"9_CR18","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1023\/A:1008723125149","volume":"14","author":"C.N. Ip","year":"1999","unstructured":"Ip, C.N., Dill, D.L.: Verifying Systems with Replicated Components in Mur&b.phiv. Formal Methods in System Design\u00a014(3), 273\u2013310 (1999)","journal-title":"Formal Methods in System Design"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-540-73368-3_16","volume-title":"Computer Aided Verification","author":"B. Jonsson","year":"2007","unstructured":"Jonsson, B., Saksena, M.: Systematic Acceleration in Regular Model Checking. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 131\u2013144. Springer, Heidelberg (2007)"},{"issue":"1","key":"9_CR20","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10703-006-4342-y","volume":"28","author":"Y. Kesten","year":"2006","unstructured":"Kesten, Y., Pnueli, A., Raviv, L., Shahar, E.: Model Checking with Strong Fairness. Formal Methods and System Design\u00a028(1), 57\u201384 (2006)","journal-title":"Formal Methods and System Design"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic Verification of Parameterized Linear Networks of Processes. In: POPL, pp. 346\u2013357 (1997)","DOI":"10.1145\/263699.263747"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Nitsche, U., Wolper, P.: Relative Liveness and Behavior Abstraction (Extended Abstract). In: PODC 1997, pp. 45\u201352 (1997)","DOI":"10.1145\/259380.259419"},{"key":"9_CR23","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.D.: Liveness with (0, 1, infty)-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"issue":"8","key":"9_CR24","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1109\/71.406955","volume":"6","author":"F. Pong","year":"1995","unstructured":"Pong, F., Dubois, M.: A New Approach for the Verification of Cache Coherence Protocols. IEEE Trans. Parallel Distrib. Syst.\u00a06(8), 773\u2013787 (1995)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"1","key":"9_CR25","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F. Pong","year":"1996","unstructured":"Pong, F., Dubois, M.: Verification Techniques for Cache Coherence Protocols. ACM Comput. Surv.\u00a029(1), 82\u2013126 (1996)","journal-title":"ACM Comput. Surv."},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"CAV 2009","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-88194-0_4","volume-title":"Formal Methods and Software Engineering","author":"J. Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S., Wang, H.H.: Specifying and verifying event-based fairness enhanced systems. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 318\u2013337. Springer, Heidelberg (2008)"},{"key":"9_CR28","unstructured":"Treiber, R.K.: Systems programming: Coping with parallelism. Technical report (1986)"},{"issue":"4","key":"9_CR29","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1002\/stvr.280","volume":"13","author":"U. Ultes-Nitsche","year":"2003","unstructured":"Ultes-Nitsche, U., St. James, S.: Improved Verification of Linear-time Properties within Fairness: Weakly Continuation-closed Behaviour Abstractions Computed from Trace Reductions. Softw. Test., Verif. Reliab.\u00a013(4), 241\u2013255 (2003)","journal-title":"Softw. Test., Verif. Reliab."}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:43Z","timestamp":1606186063000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}