{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:20:55Z","timestamp":1725492055997},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540756972"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75698-9_23","type":"book-chapter","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T02:26:03Z","timestamp":1191464763000},"page":"350-363","source":"Crossref","is-referenced-by-count":1,"title":["Implication-Based Approximating Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Zhenyu","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhihong","family":"Tao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Baowen","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lifu","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Cpmputers\u00a058 (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"issue":"1","key":"23_CR2","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11390-007-9004-z","volume":"22","author":"Z.H. Tao","year":"2007","unstructured":"Tao, Z.H., Zhou, C.H., Chen, Z., Wang, L.F.: Bounded Model Checking of CTL*. Journal of Computer Science and Technology\u00a022(1), 39\u201343 (2007)","journal-title":"Journal of Computer Science and Technology"},{"issue":"5","key":"23_CR3","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/3-540-36126-X_3","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Chauhan","year":"2002","unstructured":"Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT based Conflict Analysis. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 33\u201351. Springer, Heidelberg (2002)"},{"key":"23_CR5","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1109\/HLDVT.2005.1568832","volume-title":"Proceedings of the 10th IEEE International High-Level Design Validation and Test Workshop","author":"Z.Y. Chen","year":"2005","unstructured":"Chen, Z.Y., Zhou, C.H., Ding, D.C.: Automatic abstraction refinement for Petri nets verification. In: Proceedings of the 10th IEEE International High-Level Design Validation and Test Workshop, pp. 168\u2013174. IEEE, Los Alamitos (2005)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/11513988_11","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2005","unstructured":"Gupta, A., Strichman, O.: Abstraction refinement for bounded model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 112\u2013124. Springer, Heidelberg (2005)"},{"key":"23_CR8","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of the 2nd international Joint Conference on Artificial Intelligence, pp. 481\u2013489 (1971)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-3-540-24730-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Ravi","year":"2004","unstructured":"Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 31\u201345. Springer, Heidelberg (2004)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11750321_25","volume-title":"Theory and Applications of Models of Computation","author":"Z.Y. Chen","year":"2006","unstructured":"Chen, Z.Y., Ding, D.C.: Variable Minimal Unsatisfiability. In: Cai, J.-Y., Cooper, S.B., Li, A. (eds.) TAMC 2006. LNCS, vol.\u00a03959, pp. 262\u2013273. Springer, Heidelberg (2006)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","first-page":"546","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Shoham","year":"2003","unstructured":"Shoham, S., Grumberg, O.: Monotonic Abstraction-Refinement for CTL. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 546\u2013560. Springer, Heidelberg (2003)"},{"issue":"3","key":"23_CR12","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"23_CR13","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":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/978-3-540-30476-0_11","volume-title":"Automated Technology for Verification and Analysis","author":"S. Ogata","year":"2004","unstructured":"Ogata, S., Tsuchiya, T., Kikuno, T.: SAT-based Verification of Safe Petri Nets. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 79\u201392. Springer, Heidelberg (2004)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/3-540-44685-0_15","volume-title":"CONCUR 2001 - Concurrency Theory","author":"K. Heljanko","year":"2001","unstructured":"Heljanko, K.: Bounded Reachability Checking with Process Semantics. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 218\u2013232. Springer, Heidelberg (2001)"},{"issue":"4","key":"23_CR16","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"Murata, T.: Petri nets: Properties, Analysis and Applications. IEEE\u00a077(4), 541\u2013580 (1989)","journal-title":"IEEE"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/3-540-63166-6_43","volume-title":"Computer Aided Verification","author":"B. Grahlmann","year":"1997","unstructured":"Grahlmann, B.: The PEP Tool. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 440\u2013443. Springer, Heidelberg (1997)"},{"issue":"4","key":"23_CR18","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A New Symbolic Model Checker. International Journal on Software Tools for Technology Transfer\u00a02(4), 410\u2013425 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","International Symposium on Fundamentals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75698-9_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:27:35Z","timestamp":1619519255000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75698-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540756972"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75698-9_23","relation":{},"subject":[]}}