{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:26:13Z","timestamp":1725456373897},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028753","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"293-304","source":"Crossref","is-referenced-by-count":54,"title":["Generating finite-state abstractions of reactive systems using decision procedures"],"prefix":"10.1007","author":[{"given":"Michael A.","family":"Col\u00f3n","sequence":"first","affiliation":[]},{"given":"Tom\u00e1s E.","family":"Uribe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger, editors. Proc. 8 th Intl. Conference on Computer Aided Verification, vol. 1102 of LNCS. Springer-Verlag, July 1996.","DOI":"10.1007\/3-540-61474-5"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"N.S. Bj\u00f8rner, A. Browne, E.S. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Alur and Henzinger [AH96], pages 415-418.","DOI":"10.1007\/3-540-61474-5_92"},{"issue":"1","key":"28_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N.S. Bj\u00f8rner","year":"1997","unstructured":"N.S. Bj\u00f8rner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):49\u201387, February 1997. Preliminary version appeared in 1st Intl. Conf. on Principles and Practice of Constraint Programming, vol. 976 of LNCS, pp. 589\u2013623, Springer-Verlag, 1995.","journal-title":"Theoretical Computer Science"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"N.S. Bj\u00f8rner, M.E. Stickel, and T.E. Uribe. A practical integration of first-order reasoning and decision procedures. In 14th Intl. Conf. on Automated Deduction, vol. 1249 of LNCS, pages 101\u2013115. Springer-Verlag, July 1997.","DOI":"10.1007\/3-540-63104-6_13"},{"key":"28_CR5","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 4th ACM Symp. Princ. of Prog. Lang., pages 238\u2013252. ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"issue":"5","key":"28_CR6","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. on Prog. Lang. and Systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"key":"28_CR7","unstructured":"D.R. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, July 1996."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"J. Dingel and T. Filkorn. Model checking of infinite-state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In Wolper [Wo195], pages 54-69.","DOI":"10.1007\/3-540-60045-0_40"},{"issue":"2","key":"28_CR9","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D.R. Dams","year":"1997","unstructured":"D.R. Dams, R. Gerth, and O. Gr\u00fcmberg. Abstract interpretation of reactive systems. ACM Transactions on Prog. Lang. and Systems, 19(2):253\u2013291, 1997.","journal-title":"ACM Transactions on Prog. Lang. and Systems"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"P.R. D'Argenio, J.P. Katoen, T. Ruys, and G.T. Tretmans. The bounded retransmission protocol must be on time! In 3rd TACAS Workshop, vol. 1217 of LNCS, pages 416\u2013432. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0035403"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"D.L. Dill and H. Wong-Toi. Verification of real-time systems by successive over and under approximation. In Wolper [Wo195], pages 409\u2013422.","DOI":"10.1007\/3-540-60045-0_66"},{"key":"28_CR12","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, vol. B","author":"E.A. Emerson","year":"1990","unstructured":"E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, pages 995\u20131072. Elsevier Science Publishers (North-Holland), 1990."},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"O. Grumberg, editor. Proc. 9 th Intl. Conference on Computer Aided Verification, vol. 1254 of LNCS. Springer-Verlag, June 1997.","DOI":"10.1007\/3-540-63166-6"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Grumberg [Gru97], pages 72\u201383.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe, pages 662\u2013681, March 1996.","DOI":"10.1007\/3-540-60973-3_113"},{"key":"28_CR16","series-title":"Technical Report 95\/31","volume-title":"Practical symbolic model checking of the full \u03bc-calculus using compositional abstractions","author":"P. Kelb","year":"1995","unstructured":"P. Kelb, D. Dams, and R. Gerth. Practical symbolic model checking of the full \u03bc-calculus using compositional abstractions. Technical Report 95\/31, Eindhoven University of Technology, The Netherlands, October 1995."},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In A Decade of Concurrency, vol. 803 of LNCS, pages 273\u2013346. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58043-3_22"},{"key":"28_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1\u201335, 1995.","journal-title":"Formal Methods in System Design"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Pub., 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"28_CR20","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":"28_CR21","unstructured":"Z. Manna and A. Pnueli. Clocked transition systems. Tech. Report STAN-CSTR-96-1566, Computer Science Department, Stanford University, April 1996."},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"A. Pardo and G. Hachtel. Automatic abstraction techniques for propositional \u03bc-calculus model checking. In Grumberg [Gru97], pages 12\u201323.","DOI":"10.1007\/3-540-63166-6_5"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"H.B. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. In Alur and Henzinger [AH96], pages 208\u2013219.","DOI":"10.1007\/3-540-61474-5_70"},{"key":"28_CR24","doi-asserted-by":"crossref","unstructured":"P. Wolper, editor. Proc. 7 th Intl. Conference on Computer Aided Verification, vol. 939 of LNCS. Springer-Verlag, July 1995.","DOI":"10.1007\/3-540-60045-0"},{"key":"28_CR25","doi-asserted-by":"crossref","unstructured":"H. Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Computer Science Department, Stanford University, March 1995. Tech. Report CS-TR-95-1546.","DOI":"10.1142\/9789812831583_0007"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028753","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:23:29Z","timestamp":1586593409000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028753"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0028753","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}