{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:40:52Z","timestamp":1725496852825},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48168-0_11","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T11:30:26Z","timestamp":1196508626000},"page":"141-156","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Verifying Liveness by Augmented Abstraction"],"prefix":"10.1007","author":[{"given":"Yonit","family":"Kesten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"11_CR1","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201992","author":"S. Bensalem","year":"1992","unstructured":"S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Properties preserving simulations. CAV\u201992, LNCS 663."},{"key":"11_CR2","series-title":"Lect Notes Comput Sci","volume-title":"1st Intl. Conf. on Principles and Practice of Constraint Programming","author":"N. Bj\u00f8rner","year":"1995","unstructured":"N. Bj\u00f8rner, I.A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In 1st Intl. Conf. on Principles and Practice of Constraint Programming, LNCS 967, 1995."},{"key":"11_CR3","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Abstractions of infinite state systems compositionally and automatically. CAV\u201998, LNCS 1427."},{"key":"11_CR4","series-title":"Lect Notes Comput Sci","volume-title":"FSTTSC\u201995","author":"I.A. Browne","year":"1995","unstructured":"I.A. Browne, Z. Manna, and H.B. Sipma. Generalized verification diagrams. In FSTTSC\u201995, LNCS 1026."},{"key":"11_CR5","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL\u201977."},{"key":"11_CR6","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201994","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at ltl model checking. CAV\u201994, LNCS 818."},{"issue":"5","key":"11_CR7","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Trans. Prog. Lang. Sys., 16(5):1512\u20131542, 1994.","journal-title":"ACM Trans. Prog. Lang. Sys"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking. In Model Checking, Abstraction and Composition, volume 152 of Nato ASI Series F, pages 477\u2013498. Springer-Verlag, 1996.","DOI":"10.1007\/978-3-642-61455-2_16"},{"key":"11_CR9","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. POPL\u201978."},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Prog. Lang. Sys., 19(2), 1997.","DOI":"10.1145\/244795.244800"},{"key":"11_CR11","first-page":"83","volume":"66","author":"O. Grumberg","year":"1985","unstructured":"O. Grumberg, N. Francez, J.A. Makowski, and W.-P. de Roever. A proof rule for fair termination. Inf. and Comp., 66:83\u2013101, 1985.","journal-title":"Inf. and Comp"},{"key":"11_CR12","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201993","author":"S. Graf","year":"1993","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. CAV\u201993, LNCS 697."},{"key":"11_CR13","unstructured":"Y. Kesten and A. Pnueli. Deductive verification of fair discrete systems. Technical report, the Weizmann Institute, 1998."},{"key":"11_CR14","series-title":"Lect Notes Comput Sci","volume-title":"MFCS\u201998","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten and A. Pnueli. Modularization and Abstraction: The Keys to Formal Verification. MFCS\u201998, LNCS 1450."},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201998","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. ICALP\u201998, LNCS 1443."},{"key":"11_CR16","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. POPL\u201985."},{"key":"11_CR17","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201981","author":"D. Lehmann","year":"1981","unstructured":"D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In ICALP\u201981, LNCS 115."},{"key":"11_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. Colon, L. De Alfaro, H. Devarajan, H. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, 1994."},{"key":"11_CR19","unstructured":"Z. Manna, A. Brown, H. B. Sipma, and T. E. Uribe. Visual abstractions for temporal verification. AMAST\u201998."},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97\u2013130, 1991.","journal-title":"Theor. Comp. Sci"},{"key":"11_CR21","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991."},{"key":"11_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_123","volume-title":"Theoretical Aspects of Computer Software","author":"Z. Manna","year":"1994","unstructured":"Z. Manna and A. Pnueli. Temporal verification diagrams. In Theoretical Aspects of Computer Software, LNCS 789, 1994."},{"key":"11_CR23","doi-asserted-by":"publisher","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":"11_CR24","unstructured":"H.B. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. CAV\u201996."},{"key":"11_CR25","unstructured":"T. E. Uribe. Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Stanford University, 1999."},{"key":"11_CR26","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"M. Y. Vardi","year":"1991","unstructured":"M. Y. Vardi. Verification of concurrent programs-the automata-theoretic framework. Annals of Pure Applied Logic, 51:79\u201398, 1991.","journal-title":"Annals of Pure Applied Logic"},{"key":"11_CR27","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS\u201986."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T02:23:00Z","timestamp":1684117380000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}