{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:30Z","timestamp":1725540510429},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_22","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"426-445","source":"Crossref","is-referenced-by-count":9,"title":["Scalable Multi-core Model Checking Fairness Enhanced Systems"],"prefix":"10.1007","author":[{"given":"Yang","family":"Liu","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/11795490_10","volume-title":"Principles of Distributed Systems","author":"D. Angluin","year":"2006","unstructured":"Angluin, D., Aspnes, J., Fischer, M.J., Jiang, H.: Self-stabilizing Population Protocols. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol.\u00a03974, pp. 103\u2013117. Springer, Heidelberg (2006)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-73370-6_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2007","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Scalable Multi-core LTL Model-Checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 187\u2013203. Springer, Heidelberg (2007)"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Barnat, J., Chaloupka, J., Van De Pol, J.: Distributed Algorithms for SCC Decomposition. Journal of Logic and Computation (to appear, 2009)","DOI":"10.1093\/logcom\/exp003"},{"issue":"1","key":"22_CR4","first-page":"63","volume":"198","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Chaloupka, J., van de Pol, J.: Improved Distributed Algorithms for SCC Decomposition. ENTCS\u00a0198(1), 63\u201377 (2008)","journal-title":"ENTCS"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-70952-7_22","volume-title":"Formal Methods: Applications and Technology","author":"J. Barnat","year":"2007","unstructured":"Barnat, J., Moravec, P.: Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 316\u2013330. Springer, Heidelberg (2007)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/978-3-540-30494-4_25","volume-title":"Formal Methods in Computer-Aided Design","author":"L. Brim","year":"2004","unstructured":"Brim, L., Cerna, I., Moravec, P., Simsa, J.: Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 352\u2013366. Springer, Heidelberg (2004)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45294-X_9","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"L. Brim","year":"2001","unstructured":"Brim, L., Cern\u00e1, I., Krc\u00e1l, P., Pel\u00e1nek, R.: Distributed LTL Model Checking Based on Negative Cycle Detection. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, p. 96. Springer, Heidelberg (2001)"},{"key":"22_CR8","unstructured":"Brim, L., Cerna, I., Moravec, P., Simsa, J.: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. In: Proceedings of 4th International Workshop on Parallel and Distributed Methods in verification, pp. 1\u201312 (2005)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Cerna, I., Mu, F., Cerna, I., Cerna, I., Pelnek, R., Pelanek, R.: Distributed explicit fair cycle detection: Set based approach (2002)","DOI":"10.1007\/3-540-44829-2_4"},{"issue":"2\/3","key":"22_CR10","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design\u00a01(2\/3), 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"key":"22_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)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45319-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Fisler","year":"2001","unstructured":"Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is There a Best Symbolic Cycle-Detection Algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"issue":"1","key":"22_CR13","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. Theoritical Computer Science\u00a0345(1), 60\u201382 (2005)","journal-title":"Theoritical Computer Science"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Magee, J., Kramer, J.: Checking Progress with Action Priority: Is it Fair. In: Proceedings of the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 1999), pp. 511\u2013527 (1999)","DOI":"10.1007\/3-540-48166-4_31"},{"key":"22_CR15","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":"22_CR16","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":"10","key":"22_CR17","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G.J. Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bosnacki, D.: The Design of a Multicore Extension of the SPIN Model Checker. IEEE Trans. Softw. Eng.\u00a033(10), 659\u2013674 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On Nested Depth-first Search. In: The Spin Verification System, pp. 23\u201332 (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"issue":"2","key":"22_CR19","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10703-006-0008-z","volume":"29","author":"C.P. Inggs","year":"2006","unstructured":"Inggs, C.P., Barringer, H.: CTL* Model Checking on a Shared-memory Architecture. Form. Methods Syst. Des.\u00a029(2), 135\u2013155 (2006)","journal-title":"Form. Methods Syst. Des."},{"issue":"1","key":"22_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":"22_CR21","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1995","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton university press, Princeton (1995)"},{"key":"22_CR22","unstructured":"Lafuente, A.L.: Simplified Distributed LTL Model Checking by Localizing Cycles. Technical report, Institute of Computer Science, Albert-Ludwings Universit\u00e4t Freiburg (2002)"},{"issue":"4","key":"22_CR23","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/PL00008921","volume":"13","author":"L. Lamport","year":"2000","unstructured":"Lamport, L.: Fairness and Hyperfairness. Distributed Computing\u00a013(4), 239\u2013245 (2000)","journal-title":"Distributed Computing"},{"issue":"2","key":"22_CR24","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. IEEE Transactions on Software Engineering\u00a03(2), 125\u2013143 (1977)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/3-540-10843-2_22","volume-title":"Automata, Languages and Programming","author":"D.J. Lehmann","year":"1981","unstructured":"Lehmann, D.J., Pnueli, A., Stavi, J.: Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol.\u00a0115, pp. 264\u2013277. Springer, Heidelberg (1981)"},{"key":"22_CR26","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/1375581.1375625","volume-title":"ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008)","author":"M. Musuvathi","year":"2008","unstructured":"Musuvathi, M., Qadeer, S.: Fair Stateless Model Checking. In: ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008), pp. 362\u2013371. ACM, New York (2008)"},{"key":"22_CR27","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":"5","key":"22_CR28","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0020-0190(85)90024-9","volume":"20","author":"J.H. Reif","year":"1985","unstructured":"Reif, J.H.: Depth-First Search is Inherently Sequential. Information Processing Letters\u00a020(5), 229\u2013234 (1985)","journal-title":"Information Processing Letters"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.Q.: Integrating Specification and Programs for System Modeling and Verification. In: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pp. 127\u2013135 (2009)","DOI":"10.1109\/TASE.2009.32"},{"key":"22_CR30","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: Towards a Toolkit for Flexible and Efficient Verification under Fairness. Technical Report TRB2\/09, National Univ. of Singapore (December 2008), http:\/\/www.comp.nus.edu.sg\/~pat\/report.ps"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Proceedings of the 21th International Conference on Computer Aided Verification (CAV 2009), Grenoble, France, pp. 702\u2013708 (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"22_CR32","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":"22_CR33","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"2","author":"R. Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first Search and Linear Graph Algorithms. SIAM Journal on Computing\u00a02, 146\u2013160 (1972)","journal-title":"SIAM Journal on Computing"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:54:54Z","timestamp":1606186494000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}