{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T14:01:49Z","timestamp":1725544909405},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_14","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T14:39:50Z","timestamp":1265899190000},"page":"155-168","source":"Crossref","is-referenced-by-count":4,"title":["Model Checking with Formula-Dependent Abstract Models"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Asteroth","sequence":"first","affiliation":[]},{"given":"Christel","family":"Baier","sequence":"additional","affiliation":[]},{"given":"Ulrich","family":"A*Bmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"14_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Verification of infinite state systems by combining abstraction and reachability analysis","author":"P. Abdulla","year":"1999","unstructured":"P. Abdulla, A. Annichini, S. Bensalem, A. Boujjani, P. Habermehl, Y. Lakhnech. Verification of infinite state systems by combining abstraction and reachability analysis. In Proc. CAV\u201999, LNCS 1633, 1999."},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur, D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"14_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-58179-0_65","volume-title":"Formula-dependent equivalence for compositional CTL model checking","author":"A. Aziz","year":"1994","unstructured":"A. Aziz, T. R. Shiple, V. Singhal, A. L. Sangiovanni-Vincentelli. Formula-dependent equivalence for compositional CTL model checking. Proc. CAV\u201994, LNCS 818, pp. 324\u2013337, 1994."},{"doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, M. Fujita, Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conference, pp.317\u2013320, 1999.","key":"14_CR4","DOI":"10.21236\/ADA360973"},{"issue":"1-2","key":"14_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. Browne","year":"1988","unstructured":"M. Browne, E. Clarke, O. Grumberg. Characterizing finite Kripke structures in Propositional Temporal Logic. Theoretical Computer Science, 59(1-2):115\u2013131, July 1988.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, L. Hwang. Symbolic model checking 1020 states and beyond. Information and Computation, 1992.","key":"14_CR6","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"14_CR7","series-title":"Lect Notes Comput Sci","first-page":"197","volume-title":"Minimal model generation","author":"A. Bouajjani","year":"1990","unstructured":"A. Bouajjani, Jean-Claude Fernandez, N. Halbwachs. Minimal model generation. Proc. CAV\u201990, LNCS 531, pp. 197\u2013203, 1990."},{"key":"14_CR8","series-title":"Computing Science Reports","volume-title":"Simulation based minimization","author":"D. Bustan","year":"2000","unstructured":"D. Bustan, O. Grumberg. Simulation based minimization. Computing Science Reports CS-2000-04, Computer Science Department, Technion, Haifa 32000, Israel, 2000."},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computing abstractions of infinite state systems compositionally and automatically","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, S. Owre. Computing abstractions of infinite state systems compositionally and automatically. LNCS 1427, Proc. CAV\u201998, pp. 319\u2013331, 1998."},{"key":"14_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/3-540-56922-7_4","volume-title":"An iterative approach to language containment","author":"F. Balarin","year":"1993","unstructured":"F. Balarin, A. Sangiovanni-Vincentelli. An iterative approach to language containment. Proc. CAV\u201993, LNCS 697, pp. 29\u201340, 1993."},{"doi-asserted-by":"crossref","unstructured":"P. Cousot, R. Cousot. Abstract interpretation a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. POPL\u201977, pp. 238\u2013252, 1977.","key":"14_CR11","DOI":"10.1145\/512950.512973"},{"key":"14_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Counterexample-guided abstraction refinement","author":"E. Clarke","year":"2000","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-guided abstraction refinement. LNCS 1855, Proc. CAV\u201900, pp. 154\u2013169, 2000."},{"issue":"5","key":"14_CR13","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"unstructured":"E. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press, 2000.","key":"14_CR14"},{"key":"14_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-48153-2_14","volume-title":"Abstract BDDs: a technique for using abstraction in model checking","author":"E. Clarke","year":"1999","unstructured":"E. Clarke, S. Jha, Y. Lu, D. Wang. Abstract BDDs: a technique for using abstraction in model checking. In Proc. Correct Hardware Design and Verification Methods, LNCS 1703, pp. 172\u2013186, 1999."},{"unstructured":"D. Dams. Abstract Interpretation and Partition Refinement forModel Checking. PhD thesis, Technische Universiteit Einhoven, 1996.","key":"14_CR16"},{"key":"14_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-60045-0_40","volume-title":"Model checking for infinite state systems using data abstraction, assumption commitment style reasoning and theorem proving","author":"J. Dingel","year":"1995","unstructured":"J. Dingel, T. Filkorn. Model checking for infinite state systems using data abstraction, assumption commitment style reasoning and theorem proving. In Proc. CAV\u201995, LNCS 939, pp. 54\u201369, 1995."},{"key":"14_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/3-540-56922-7_39","volume-title":"Generation of reduced models for checking fragments of CTL","author":"D. Dams","year":"1993","unstructured":"D. Dams, R. Gerth, O. Grumberg. Generation of reduced models for checking fragments of CTL. In Proc. CAV\u201993, LNCS 697, pp. 479\u2013490, 1993."},{"issue":"2","key":"14_CR19","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"D. Dams, R. Gerth, O. Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253\u2013291, March 1997.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR20","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics","author":"E. A. Emerson","year":"1990","unstructured":"E. A. Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 995\u20131072. Elsevier Science Publishers, Amsterdam, The Netherlands, 1990."},{"issue":"3","key":"14_CR21","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg, D. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial order methods for the verification of concurrent systems: An approach to the state explosion problem","author":"P. Godefroid","year":"1996","unstructured":"P. Godefroid. Partial order methods for the verification of concurrent systems: An approach to the state explosion problem (Ph.D.Thesis, University of Liege) LNCS 1032, 1996."},{"key":"14_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Construction of abstract state graphs with PVS","author":"S. Graf","year":"1997","unstructured":"S. Graf, H. Saidi. Construction of abstract state graphs with PVS. In Proc. CAV\u201997, LNCS 1254, pp 72\u201383, 1997."},{"doi-asserted-by":"crossref","unstructured":"M. Henzinger, T. Henzinger, P. Kopke. Computing simulations on finite and infinite graphs. In Proc. FOCS\u201995, pp. 453\u2013462, IEEE Computer Society Press. 1995.","key":"14_CR24","DOI":"10.1109\/SFCS.1995.492576"},{"unstructured":"P. Kelb, D. Dams, R. Gerth. Efficient symbolic model checking of the full \u00b5-calculus using compositional abstractions. Computing Science Reports 95\/31, Eindhoven University of Technology, 1995.","key":"14_CR25"},{"doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.","key":"14_CR26","DOI":"10.1515\/9781400864041"},{"issue":"1","key":"14_CR27","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1):11\u201344, January 1995.","journal-title":"Formal Methods in System Design"},{"key":"14_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-48683-6_28","volume-title":"Stepwise CTL model checking of State\/Event systems","author":"J. Lind-Nielsen","year":"1999","unstructured":"J. Lind-Nielsen, H. Andersen. Stepwise CTL model checking of State\/Event systems. In Proc. CAV\u201999, LNCS 1633, pp. 316\u2013327, 1999."},{"unstructured":"D. Long. Model Checking, Abstraction and Compositional Verification. PhD thesis, Carnegie Mellon University, 1993.","key":"14_CR29"},{"doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97\u2013107, New York, January 1985. ACM.","key":"14_CR30","DOI":"10.1145\/318593.318622"},{"unstructured":"W. Lee, A. Pardo, J.-Y. Jang, G. Hachtel, F. Somenzi. Tearing based automatic abstraction for ctl model checking. In Proc. ICCAD\u201996, pp. 76\u201381, 1996.","key":"14_CR31"},{"doi-asserted-by":"crossref","unstructured":"D. Lee, M. Yannakakis. Online minimization of transition systems. In Proc. STOC\u201992, pp. 264\u2013274, 1992. ACM Press.","key":"14_CR32","DOI":"10.1145\/129712.129738"},{"doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","key":"14_CR33","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"14_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"Syntactic program transformation for automatic abstraction","author":"K. Namjoshi","year":"2000","unstructured":"K. Namjoshi, R. Kurshan. Syntactic program transformation for automatic abstraction. In Proc. CAV\u20192000, LNCS 1855, pp. 435\u2013449, 2000."},{"key":"14_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"All from one, one from all: on model checking using representatives","author":"D. Peled","year":"1993","unstructured":"D. Peled. All from one, one from all: on model checking using representatives. In Proc. CAV\u201993, LNCS 697, pp. 409\u2013423, 1993."},{"key":"14_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/3-540-63166-6_5","volume-title":"Automatic abstraction techniques for propositional \u00b5-calculus model checking","author":"A. Pardo","year":"1997","unstructured":"A. Pardo, G. Hachtel. Automatic abstraction techniques for propositional \u00b5-calculus model checking. In Proc. CAV\u201997, LNCS 1254, pp. 12\u201323, 1997."},{"issue":"6","key":"14_CR37","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"R. Paige, R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973\u2013989, 1987.","journal-title":"SIAM Journal on Computing"},{"key":"14_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Abstract and model check while you prove","author":"H. Saidi","year":"1999","unstructured":"H. Saidi, N. Shankar. Abstract and model check while you prove. In Proc. CAV\u201999, LNCS 1633, pp 443\u2013454, 1999."},{"key":"14_CR39","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/3-540-61474-5_70","volume-title":"Deductive Model Checking","author":"H. B. Sipma","year":"1996","unstructured":"H. B. Sipma, T. E. Uribe, Z Manna. Deductive Model Checking. In Proc. CAV\u201996, LNCS 1102, pp. 208\u2013219, 1996"},{"key":"14_CR40","first-page":"6","volume":"46","author":"A. Valmari","year":"1994","unstructured":"A. Valmari. State of the art report: Stubborn sets. Petri-Net Newsletters, 46:6\u201314, 1994.","journal-title":"Petri-Net Newsletters"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T18:29:28Z","timestamp":1558808968000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}