{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:21:14Z","timestamp":1725560474693},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213147"},{"type":"electronic","value":"9783540247326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_15","type":"book-chapter","created":{"date-parts":[[2010,7,28]],"date-time":"2010-07-28T00:14:47Z","timestamp":1280276087000},"page":"198-215","source":"Crossref","is-referenced-by-count":5,"title":["Using Fairness to Make Abstractions Work"],"prefix":"10.1007","author":[{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natalia","family":"Ioustinova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natalia","family":"Sidorova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"15_CR1","first-page":"141","volume":"7","author":"K. Baukus","year":"2001","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Verification of parameterized protocols. Journal of Universal Computer Science\u00a07(2), 141\u2013158 (2001)","journal-title":"Journal of Universal Computer Science"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-48234-2_4","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"D. Bo\u0161na\u010dki","year":"1999","unstructured":"Bo\u0161na\u010dki, D.: Partial-order reduction in presence of rendez-vous communication with unless constructs and weak fairness. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, p. 40. Springer, Heidelberg (1999)"},{"key":"15_CR3","volume-title":"Proc. of Formal Description Techniques and Protocol Specification, Testing, and Verification","author":"D. Bo\u0161na\u010dki","year":"1998","unstructured":"Bo\u0161na\u010dki, D., Dams, D.: Integrating real time into Spin: A prototype implementation. In: Proc. of Formal Description Techniques and Protocol Specification, Testing, and Verification, Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46419-0_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Bo\u0161na\u010dki","year":"2000","unstructured":"Bo\u0161na\u010dki, D., Dams, D., Holenderski, L., Sidorova, N.: Verifying SDL in Spin. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 363. Springer, Heidelberg (2000)"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Choueka, Y.: Theories of automata on \u03c9-tapes: a simplified approach. Journal of Computer and System Science\u00a08, 117\u2013141 (1974)","journal-title":"Journal of Computer and System Science"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Int. Conference on Computer Aided Verification (CAV 2000)","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design\u00a01, 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"key":"15_CR8","volume-title":"Proc. of POPL 1973","author":"P. Cousot","year":"1973","unstructured":"Cousot, P., Cousot, R.: Abstract interpretaion: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL 1973, January 1973, ACM, New York (1973)"},{"key":"15_CR9","unstructured":"Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD dissertation, Eindhoven University of Thechnology (July 1996)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Dams, D., Gerth, R.: The bounded retransmission protocol revisited. Electronic Notes in Theoretical Computer Science, 9 (1999)","DOI":"10.1016\/S1571-0661(05)80425-6"},{"key":"15_CR11","series-title":"IFIP","volume-title":"Proc. of PROCOMET 1994","author":"D. Dams","year":"1994","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems: Abstraction preserving \u2200CTL\u2009\u2217\u2009, \u2203CTL\u2009\u2217\u2009, and CTL\u2009\u2217\u2009. In: Proc. of PROCOMET 1994, June 1994. IFIP, North-Holland, Amsterdam (1994)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems (TOPLAS), 19(2) (1997)","DOI":"10.1145\/244795.244800"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/3-540-46017-9_24","volume-title":"Model Checking Software","author":"M.M. Gallardo","year":"2002","unstructured":"Gallardo, M.M., Martine, J., Merino, P., Pimentel, E.: \u03b1Spin: Extending Spin with abstraction. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 254\u2013258. Springer, Heidelberg (2002)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1994","unstructured":"Graf, S.: Verification of a distributed cache memory by using abstractions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, Springer, Heidelberg (1994)"},{"key":"15_CR15","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)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/3-540-45614-7_30","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"N. Ioustinova","year":"2002","unstructured":"Ioustinova, N., Sidorova, N., Steffen, M.: Closing open SDL-systems for model checking with DT Spin. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, p. 531. Springer, Heidelberg (2002)"},{"issue":"4","key":"15_CR17","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. Int. Journal on Software Tools for Technology Transfer\u00a02(4), 328\u2013342 (2000)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation\u00a0163(1), 203\u2013243 (2000)","journal-title":"Information and Computation"},{"issue":"1","key":"15_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions in Computer Systems\u00a05(1), 1\u201311 (1987)","journal-title":"ACM Transactions in Computer Systems"},{"issue":"1","key":"15_CR20","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design\u00a06(1), 11\u201344 (1995)","journal-title":"Formal Methods in System Design"},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"B.D. Lubachevsky","year":"1984","unstructured":"Lubachevsky, B.D.: An approach to automating the verification of compact parallel coordination programs I. Acta Informatica\u00a021, 125\u2013169 (1984)","journal-title":"Acta Informatica"},{"key":"15_CR22","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.: Liveness with (0,1, \u221e)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"15_CR23","volume-title":"Computer Networks","author":"A.S. Tanenbaum","year":"1981","unstructured":"Tanenbaum, A.S.: Computer Networks. Prentice Hall Int. Inc., Englewood Cliffs (1981)"},{"key":"15_CR24","first-page":"613","volume-title":"Proc. IFIP 1989","author":"R.J. Glabbeek van","year":"1989","unstructured":"van Glabbeek, R.J., Weijland, R.P.: Branching time and abstraction in bisimulation semantics. In: Proc. IFIP 1989, pp. 613\u2013618. North-Holland, Amsterdam (1989)"},{"key":"15_CR25","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, St. Petersburgh, January 1986, pp. 184\u2013192 (1986)","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:30:18Z","timestamp":1559331018000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}