{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:26:21Z","timestamp":1726406781014},"publisher-location":"Berlin, Heidelberg","reference-count":26,"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_9","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"81-96","source":"Crossref","is-referenced-by-count":0,"title":["Interleaved Invariant Checking with Dynamic Abstraction"],"prefix":"10.1007","author":[{"given":"Liang","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Mukul R.","family":"Prasad","sequence":"additional","affiliation":[]},{"given":"Michael S.","family":"Hsiao","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-30494-4_19","volume-title":"Formal Methods in Computer-Aided Design","author":"N. Amla","year":"2004","unstructured":"Amla, N., McMillan, K.L.: A hybrid of counterexample-based and proof-based abstraction. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 260\u2013274. Springer, Heidelberg (2004)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Kukula, J.: Using Counter Example Guided Abstraction Refinement to Find Complex Bugs. In: Proc. of the Design Automation and Test in Europe, February 2004, pp. 156\u2013161 (2004)","DOI":"10.1109\/DATE.2004.1268842"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Quer, S.: Efficient State Space Pruning in Symbolic Backward Traversal. In: Proc. of the Intl. Conf. on Computer Design, October 1994, pp. 230\u2013235 (1994)","DOI":"10.1109\/ICCD.1994.331895"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/3-540-45657-0_38","volume-title":"Computer Aided Verification","author":"G. Cabodi","year":"2002","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 471. Springer, Heidelberg (2002)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.M., 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)"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45657-0_20","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Gupta, A., Kukula, J., Strichman, O.: SAT-based Abstraction Refinement Using ILP and Machine Learning Techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 265\u2013279. Springer, Heidelberg (2002)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-36577-X_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Glusman","year":"2003","unstructured":"Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 176\u2013191. Springer, Heidelberg (2003)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proc. of the Design Automation and Test in Europe, March 2003, pp. 886\u2013891 (2003)","DOI":"10.1109\/DATE.2003.1253718"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Govindaraju, S.G., Dill, D.L.: Verification by approximate forward and backward reachability. In: Proc. of Intl. Conf. on CAD, November 1998, pp. 366\u2013370 (1998)","DOI":"10.1145\/288548.289055"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative Abstraction Using SAT-based BMC with Proof Analysis. In: Proc. of the Intl. Conf. on CAD, November 2003, pp. 416\u2013423 (2003)","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Iwashita, H., Nakata, T.: Forward model checking techniques oriented to buggy designs. In: Proc. of Intl. Conf. on CAD, November 1997, pp. 400\u2013404 (1997)","DOI":"10.1109\/ICCAD.1997.643567"},{"key":"9_CR13","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1995","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1995)"},{"key":"9_CR14","unstructured":"Li, B., Somenzi, F.: Efficient Computation of Small Abstraction Refinements. In: Proc. of the Intl. Conf. on CAD (November 2004)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Mang, F.Y.-C., Ho, P.-H.: Abstraction Refinement by Controllability and Cooperativeness Analysis. In: Proc. of the Design Automation Conf., June 2004, pp. 224\u2013229 (2004)","DOI":"10.1145\/996566.996630"},{"key":"9_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-540-30494-4_29","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Stangier","year":"2004","unstructured":"Stangier, C., Sidle, T.: Invariant Checking Combining Forward and Backward Traversal. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 414\u2013429. Springer, Heidelberg (2004)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","first-page":"428","volume-title":"Computer Aided Verification","author":"The VIS Group","year":"1996","unstructured":"The VIS Group: VIS: A system for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"9_CR20","unstructured":"VIS Verilog Benchmarks, \n                    \n                      http:\/\/vlsi.colorado.edu\/~vis"},{"key":"9_CR21","unstructured":"Wang, C., Hachtel, G.D., Somenzi, F.: Fine-Grain Abstraction and Sequential Don\u2019t Cares for Large Scale Model Checking. In: Proc. of the Intl. Conf. on Computer Design (October 2004)"},{"key":"9_CR22","unstructured":"Wang, C., Li, B., Jin, H., Hachtel, G.D., Somenzi, F.: Improving Ariadne\u2019s Bundle by Following Multiple Threads in Abstraction Refinement. In: Proc. of the Intl. Conf. on CAD, November 2003, pp. 408\u2013415 (2003)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Wang, D., Ho, P.-H., Long, J., Kukula, J., Zhu, Y., Ma, T., Damiano, R.: Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines. In: Proc. of the Design Automation Conf., June 2001, pp. 35\u201340 (2001)","DOI":"10.1145\/378239.378260"},{"key":"9_CR24","unstructured":"http:\/\/ee.princeton.edu\/~chaff\/zchaff.php\n                    \n                    \n                   (December 2003)"},{"key":"9_CR25","unstructured":"Zhang, L., Malik, S.: Validating SAT Solvers using an Independent Resolution-based Checker: Practical Implementations and Other Applications. In: Proc. of the Design Automation and Test in Europe, March 2003, pp. 880\u2013885 (2003)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, L., Prasad, M.R., Hsiao, M., Sidle, T.: Dynamic Abstraction Using SAT-based BMC. In: Proc. of the Design Automation Conf., June 2005, pp. 754\u2013757 (2005)","DOI":"10.1145\/1065579.1065776"}],"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_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:13:15Z","timestamp":1619507595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11560548_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}