{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:15:08Z","timestamp":1742379308643},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_8","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"65-80","source":"Crossref","is-referenced-by-count":12,"title":["How Thorough Is Thorough Enough?"],"prefix":"10.1007","author":[{"given":"Arie","family":"Gurfinkel","sequence":"first","affiliation":[]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G. Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 274\u2013287. Springer, Heidelberg (1999)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-44618-4_14","volume-title":"CONCUR 2000 - Concurrency Theory","author":"G. Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized Model Checking: Reasoning About Partial State Spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 168\u2013182. Springer, Heidelberg (2000)"},{"issue":"4","key":"8_CR4","first-page":"1","volume":"12","author":"M. Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model-Checking. ACM Trans. on Soft. Eng. and Methodology\u00a012(4), 1\u201338 (2003)","journal-title":"ACM Trans. on Soft. Eng. and Methodology"},{"issue":"5","key":"8_CR5","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"Journal of the ACM"},{"key":"8_CR6","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"2","key":"8_CR7","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 Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. on Prog. Lang. and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"key":"8_CR8","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 the 4th POPL, Los Angeles, California, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"19","key":"8_CR9","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"2","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM Trans. on Prog. Lang. and Systems\u00a02(19), 253\u2013291 (1997)","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"key":"8_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-45656-2_15","volume-title":"AI 2001: Advances in Artificial Intelligence","author":"T. French","year":"2001","unstructured":"French, T.: Decidability of Quantifed Propositional Branching Time Logics. In: Stumptner, M., Corbett, D.R., Brooks, M. (eds.) Canadian AI 2001. LNCS (LNAI), vol.\u00a02256, pp. 165\u2013176. Springer, Heidelberg (2001)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-Based Model Checking Using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45657-0_11","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Jagadeesan, R.: Automatic Abstraction Using Generalized Model-Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 137\u2013150. Springer, Heidelberg (2002)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/3-540-36384-X_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Jagadeesan, R.: On the Expressiveness of 3-Valued Models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 206\u2013222. Springer, Heidelberg (2002)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"FME 2003: Formal Methods","author":"A. Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M.: Generating Counterexamples for Multi-Valued Model-Checking. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805. Springer, Heidelberg (2003)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-45187-7_18","volume-title":"CONCUR 2003 - Concurrency Theory","author":"A. Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M.: Multi-Valued Model-Checking via Classical Model-Checking. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 266\u2013280. Springer, Heidelberg (2003)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-30494-4_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: Extending Extended Vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 306\u2013321. Springer, Heidelberg (2004)"},{"key":"8_CR18","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. Van Nostrand, New York (1952)"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/logcom\/7.1.1","volume":"7","author":"O. Kupferman","year":"1997","unstructured":"Kupferman, O.: Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. J. of Logic and Computation\u00a07, 1\u201314 (1997)","journal-title":"J. of Logic and Computation"},{"key":"8_CR20","unstructured":"Milner, R.: An Algebraic Definition of Simulation between Programs. In: AI 1971, pp. 481\u2013489 (1971)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/3-540-48294-6_22","volume-title":"Static Analysis","author":"M. M\u00fcller-Olm","year":"1999","unstructured":"M\u00fcller-Olm, M., Schmidt, D., Steffen, B.: Model-Checking: A Tutorial Introduction. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 330\u2013354. Springer, Heidelberg (1999)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-45069-6_28","volume-title":"Computer Aided Verification","author":"S. Shoham","year":"2003","unstructured":"Shoham, S., Grumberg, O.: A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 275\u2013287. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:13:14Z","timestamp":1619507594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11560548_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}