{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T22:17:36Z","timestamp":1773526656667,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439974","type":"print"},{"value":"9783540456575","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_9","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T10:59:43Z","timestamp":1179572383000},"page":"107-122","source":"Crossref","is-referenced-by-count":94,"title":["Liveness with (0,1, \u221e)- Counter Abstraction"],"prefix":"10.1007","author":[{"given":"Amir","family":"Pnueli","sequence":"first","affiliation":[]},{"given":"Jessie","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. IPL, 22(6), 1986.","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV\u201901, pages 221\u2013234, 2001.","DOI":"10.1007\/3-540-44585-4_19"},{"issue":"2","key":"9_CR3","first-page":"141","volume":"7","author":"K. Baukus","year":"2001","unstructured":"K. Baukus, Y. Lakhnesche, and K. Stahl. Verification of parameterized protocols. Journal of Universal Computer Science, 7(2):141\u2013158, 2001.","journal-title":"Journal of Universal Computer Science"},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/3-540-60299-2_37","volume-title":"1st Intl. Conf. on Principles and Practice of Constraint Programming","author":"N. Bj\u00f8rner","year":"1995","unstructured":"N. Bj\u00f8rner, I. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In 1st Intl. Conf. on Principles and Practice of Constraint Programming, volume 976 of LNCS, pages 589\u2013623. Springer-Verlag, 1995."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In CONCUR\u201995, pages 395\u2013407, 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL\u2019 77. ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"E. Emerson and V. Kahlon. Reducing model checking of the many to the few. In 17th International Conference on Automated Deduction (CADE-17), pages 236\u2013255, 2000.","DOI":"10.1007\/10721959_19"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In POPL\u201995, 1995.","DOI":"10.1145\/199448.199468"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"E. Gribomont and G. Zenner. Automated verification of szymanski\u2019s algorithm. In B. Steffen, editor, TACAS\u201998, pages 424\u2013438, 1998.","DOI":"10.1007\/BFb0054187"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"V. Gyuris and A. P. Sistla. On-the-fly model checking under fairness that exploits symmetry. In CAV\u201997, 1997.","DOI":"10.1007\/3-540-63166-6_24"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"J. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In TACAS\u201995, 1995.","DOI":"10.7146\/brics.v2i21.19923"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In TACAS\u201900, 2000.","DOI":"10.1007\/3-540-46419-0_16"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In CAV\u201997, pages 424\u2013435, 1997.","DOI":"10.1007\/3-540-63166-6_41"},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"4","author":"Y. Kesten","year":"2000","unstructured":"Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of practical formal verification. Software Tools for Technology Transfer, 4(2):328\u2013342, 2000.","journal-title":"Software Tools for Technology Transfer"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL\u2019 97, Paris, 1997.","DOI":"10.1145\/263699.263747"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specification. In POPL\u201985, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"B.D. Lubachevsky. An approach to automating the verification of compact parallel coordination programs. Acta Infromatica, 21, 1984.","DOI":"10.1007\/BF00289237"},{"key":"9_CR18","volume-title":"Technical Report STAN-CS-TR-94-1518","author":"Z. Manna","year":"1994","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, L. D. Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994."},{"key":"9_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"K. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In CAV\u201998, pages 110\u2013121, 1998.","DOI":"10.1007\/BFb0028738"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In CAV\u201996, pages 184\u2013195, 1996.","DOI":"10.1007\/3-540-61474-5_68"},{"issue":"8","key":"9_CR22","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/71.406955","volume":"6","author":"F. Pong","year":"1995","unstructured":"F. Pong and M. Dubois. A new approach for the verification of cache coherence protocols. IEEE Transactions on Parallel and Distributed Systems, 6(8):773\u2013787, Aug. 1995.","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"B. K. Szymanski. A simple solution to Lamport\u2019s concurrent programming problem with linear wait. In Proc. 1988 International Conference on Supercomputing Systems, pages 621\u2013626, St. Malo, France, 1988.","DOI":"10.1145\/55364.55425"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:21:25Z","timestamp":1556414485000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}