{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:45:34Z","timestamp":1742388334634},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1007\/s10009-002-0092-3","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T15:13:37Z","timestamp":1079795617000},"page":"505-528","source":"Crossref","is-referenced-by-count":16,"title":["Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking"],"prefix":"10.1007","volume":"4","author":[{"given":"Yifei","family":"Dong","sequence":"first","affiliation":[]},{"given":"Xiaoqun","family":"Du","sequence":"additional","affiliation":[]},{"given":"Gerard J.","family":"Holzmann","sequence":"additional","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,8,1]]},"reference":[{"key":"92_CITCAV96","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Computer Aided Verification (CAV \u201996), Lecture Notes in Computer Science, vol. 1102. Springer, Berlin Heidelberg New York, 1996","DOI":"10.1007\/3-540-61474-5"},{"key":"92_CITCCA96","unstructured":"Chamillard, A.T., Clarke, L.A., Avrunin, G.S.: Experimental design for comparing static concurrency analysis techniques. Technical Report 96-084, Computer Science Department, University of Massachusetts at Amherst, 1996"},{"issue":"2","key":"92_CITClaEmeSis86","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","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):244\u2013263, 1986","journal-title":"ACM TOPLAS"},{"key":"92_CITCLSS96a","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Lewis, P.M., Smolka, S.A., Sokolsky, O.: The Concurrency Factory: a development environment for concurrent systems. In: Alur, Henzinger, (eds.), [1], pp. 398\u2013401","DOI":"10.1007\/3-540-61474-5_88"},{"key":"92_CITCM88","unstructured":"Chandy, K.M., Misra, J.: Parallel program design \u2013 a foundation. Addison-Wesley, Reading, Mass., USA, 1988"},{"issue":"3","key":"92_CITCor96","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1109\/32.489078","volume":"22","author":"J.C. Corbett","year":"1996","unstructured":"Corbett, J.C.: Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering 22(3):161\u2013180, March 1996","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"92_CITClaWin96","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future directions. ACM Comput Surv 28(4):626\u2013643, 1996","journal-title":"ACM Comput Surv"},{"key":"92_CITiprotourl","unstructured":"Dong, Y: i-Protocol case study web sitehttp:\/\/www.cs.sunysb.edu\/\u223clmc\/iproto\/, 2000"},{"key":"92_CITDDR99","doi-asserted-by":"crossref","unstructured":"Dong, Y., Du, X., Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Sokolsky, O., Stark, E.W., Warren, D.S.: Fighting livelock in the i-Protocol: a comparative study of verification tools. In: Tools and Algorithms for the Construction and Analysis of Algorithms (TACAS \u201999), Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, 1999","DOI":"10.1007\/3-540-49059-0_6"},{"key":"92_CITDill96","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: The Mur\u03d5 verification system. In: Alur, Henzinger, (eds.), [1], pp. 390\u2013393","DOI":"10.1007\/3-540-61474-5_86"},{"key":"92_CITDR99","doi-asserted-by":"crossref","unstructured":"Dong, Y., Ramakrishnan, C.R.: An optimizing compiler for efficient model checking. In: Proc. FORTE\/PSTV \u201999 1999","DOI":"10.1007\/978-0-387-35578-8_14"},{"key":"92_CITEmersonClarke","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs as fixpoints. In: Proc. 7th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 85. Springer, Berlin Heidelberg New York, 1981"},{"key":"92_CITHuDill93","doi-asserted-by":"crossref","unstructured":"Hu, A., Dill, D.: Efficient verification with BDDs using implicitly conjoined invariants. In: Courcoubetis, C., (ed.), Computer Aided Verification (CAV \u201993), Lecture Notes in Computer Science, vol. 693. Springer, Berlin Heidelberg New York, 1993, pp. 3\u201314","DOI":"10.1007\/3-540-56922-7_2"},{"key":"92_CITHHK96","doi-asserted-by":"crossref","unstructured":"Hardin, R.H., Har\u2019El, Z., Kurshan, R.P.: COSPAN. In: Alur, Henzinger, (eds.), [1], pp. 423\u2013427","DOI":"10.1007\/3-540-61474-5_94"},{"issue":"5","key":"92_CITHol97","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans Software Eng 23(5): 279\u2013295, 1997","journal-title":"IEEE Trans Software Eng"},{"key":"92_CITHol98","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: Designing executable abstractions. In: Proc. Workshop on Formal Methods in Software Practice Clearwater Beach, Fla., USA, March 1998. ACM, New York","DOI":"10.1145\/298595.298864"},{"key":"92_CITHol99","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The engineering of a model checker: the Gnu i-protocol case study revisited. In: Dams, D., Gerth, R., Leue, S., Massink, M., (eds.), Theoretical and Practical Aspects of SPIN Model Checking, Lecture Notes in Computer Science, vol. 1680. Springer, Berlin Heidelberg New York, 1999","DOI":"10.1007\/3-540-48234-2_18"},{"key":"92_CITMcMillan93","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking. Kluwer Academic, Boston, Mass., USA, 1993","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"92_CITMil89","unstructured":"Milner, R.: Communication and concurrency. International Series in Computer Science. Prentice-Hall, N.J., USA, 1989"},{"key":"92_CITQueilleSifakis","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Proc. International Symposium in Programming, Lecture Notes in Computer Science, vol. 137. Springer, Berlin Heidelberg New York, 1982","DOI":"10.1007\/3-540-11494-7_22"},{"key":"92_CITRRR97","doi-asserted-by":"crossref","unstructured":"Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T.W., Warren D.S.: Efficient model checking using tabled resolution. In: Proc. 9th International Conference on Computer-Aided Verification (CAV \u201997) Haifa, Israel, July 1997. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-63166-6_16"},{"key":"92_CITRamSmo97","doi-asserted-by":"crossref","unstructured":"Ramakrishna, Y.S., Smolka, S.A.: Partial-order reduction in the weak modal mu-calculus. In: Mazurkiewicz, A. Winkowski, J., (eds.), Proc. 8th International Conference on Concurrency Theory (CONCUR \u201997), Lecture Notes in Computer Science, vol. 1243. Springer, Berlin Heidelberg New York, 1997","DOI":"10.1007\/3-540-63141-0_2"},{"key":"92_CITspinurl","unstructured":"Spin Web Site.:http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html"},{"key":"92_CITTan96","unstructured":"Tanenbaum, A.S.: Computer networks. Prentice-Hall, Reading, Mass., USA, 1996"},{"key":"92_CITTh90","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B. Elsevier Science, Amsterdam, Holland, 1990","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"92_CITVarWol86","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science (LICS \u201986) pp. 332\u2013344, Cambridge, Mass., USA, June 1986. Computer Society, New York"},{"key":"92_CITWol86","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: Proc. 13th ACM Symp. on Principles of Programming Languages pp. 184\u2013192, St. Petersburgh, Russia, January 1986","DOI":"10.1145\/512644.512661"},{"key":"92_CITXSB","unstructured":"XSB.: The XSB logic programming system v2.01, 1999. Available by anonymous ftp at: ftp.cs.sunysb.edu"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0092-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-002-0092-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0092-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0092-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T18:10:57Z","timestamp":1585678257000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-002-0092-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["92"],"URL":"https:\/\/doi.org\/10.1007\/s10009-002-0092-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}