{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:06:29Z","timestamp":1725516389185},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540698401"},{"type":"electronic","value":"9783540698487"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69848-7_82","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"1035-1048","source":"Crossref","is-referenced-by-count":0,"title":["Formula-Dependent Abstraction for CTL Model Checking"],"prefix":"10.1007","author":[{"given":"Junyan","family":"Qian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lingzhong","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guoyong","family":"Cai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tianlong","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"82_CR1","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"82_CR2","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1098\/rsta.1992.0028","volume":"339","author":"E.M. Clarke","year":"1992","unstructured":"Clarke, E.M., Burch, J.R., Grumberg, O., Long, D.E., McMillan, K.L.: Automatic Verification of Sequential Circuit Designs. Phil. Trans. of the Royal Society of London\u00a0339, 105\u2013120 (1992)","journal-title":"Phil. Trans. of the Royal Society of London"},{"key":"82_CR3","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and Model Logic. Formal Models and Semantics. Handbook of theoretical Computer Science, vol.\u00a0B, pp. 996\u20131072 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"82_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logic of Programs: Workshop","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. In: Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"82_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proceedings of Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Proceedings of Computer Aided Verification. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"82_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"82_CR7","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation Frameworks. Journal of Logic and Computation\u00a02(4), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"82_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verfication of Finite-state Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"82_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction Refinement. In: Proceedings of Computer Aided Verification, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"issue":"1","key":"82_CR10","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1006\/inco.1995.1059","volume":"118","author":"R. Alur","year":"1995","unstructured":"Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing Verification by Successive Approximation. Information and Computation\u00a0118(1), 142\u2013157 (1995)","journal-title":"Information and Computation"},{"key":"82_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/3-540-45319-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Lakhnech","year":"2001","unstructured":"Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental Verification by Abstraction. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 98\u2013112. Springer, Heidelberg (2001)"},{"key":"82_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Long, D.E.: Model Checking and Abstraction. In: Proceedings of TOPLAS, pp. 1512\u20131542 (1994)","DOI":"10.1145\/186025.186051"},{"key":"82_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-58179-0_65","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1994","unstructured":"Aziz, A., Shiple, T.R., Singhal, V., Sangiovanni-Vincentelli, A.L.: Formula-dependent Equivalence for Compositional CTL Model Checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 324\u2013337. Springer, Heidelberg (1994)"},{"key":"82_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/3-540-56922-7_39","volume-title":"Computer Aided Verification","author":"D. Dams","year":"1993","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Generation of Reduced Models for Checking Fragments of CTL. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 479\u2013490. Springer, Heidelberg (1993)"},{"issue":"2","key":"82_CR15","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM Transactions on Programming Languages and Systems\u00a019(2), 253\u2013291 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"82_CR16","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":"82_CR17","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Fair model Checking of Abstractions (extended abstract). In: Proceedings of VCL, number DSSE-TR-2000-6, University of Southampton (July 2000)"},{"key":"82_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-58201-0_82","volume-title":"Automata, Languages, and Programming","author":"A. Aziz","year":"1994","unstructured":"Aziz, A., Singhal, V., Shiple, T.R., SangiovanniVincentelli, A.L., Balarin, F., Brayton, R.K.: Equivalences for Fair Kripke Structures. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol.\u00a0820, pp. 364\u2013375. Springer, Heidelberg (1994)"},{"key":"82_CR19","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Proceedings of Computer Aided Verification. LNCS, vol.\u00a01427, pp. 319\u2013331 (1998)","DOI":"10.1007\/BFb0028755"},{"key":"82_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"Static Analysis","author":"R. Giacobazzi","year":"2001","unstructured":"Giacobazzi, R., Ranzato, F.: Incompleteness, Counterexamples and Refinements in Abstract Model Checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 356\u2013373. Springer, Heidelberg (2001)"},{"key":"82_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/978-3-540-24725-8_3","volume-title":"Programming Languages and Systems","author":"F. Ranzato","year":"2004","unstructured":"Ranzato, F., Tapparo, F.: Strong Preservation as Completeness in Abstract Interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 18\u201332. Springer, Heidelberg (2004)"},{"key":"82_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/11609773_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F. Ranzato","year":"2005","unstructured":"Ranzato, F., Tapparo, F.: Strong Preservation of Temporal Fixpoint-based Operators by Abstract Interpretation. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 332\u2013347. Springer, Heidelberg (2005)"},{"key":"82_CR23","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proceedings of ICSE, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"issue":"4","key":"82_CR24","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model Checking JAVA Programs using JAVA PathFinder. International Journal on Software Tools for Technology Transfer\u00a02(4), 366\u2013381 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"82_CR25","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"issue":"2-3","key":"82_CR26","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:FORM.0000040026.56959.91","volume":"25","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient Verification of Sequential and Concurrent C Programs. Formal Methods in System Design\u00a025(2-3), 129\u2013166 (2004)","journal-title":"Formal Methods in System Design"},{"key":"82_CR27","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proceedings of POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2013 ICCSA 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69848-7_82.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:03:47Z","timestamp":1605762227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69848-7_82"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540698401","9783540698487"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69848-7_82","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}