{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:37:01Z","timestamp":1725550621340},"publisher-location":"Berlin, Heidelberg","reference-count":25,"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_18","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"222-237","source":"Crossref","is-referenced-by-count":8,"title":["Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies"],"prefix":"10.1007","author":[{"given":"Jason","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Hari","family":"Mony","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Jain, P., Gopalakrishnan, G.: Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. IEEE Transactions on CAD (April 1994)","DOI":"10.1109\/43.298036"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Formal verification using parametric representations of Boolean constraints. In: Design Automation Conference (June 1999)","DOI":"10.1145\/309847.309968"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Bertacco, V., Olukotun, K.: Efficient state representation for symbolic simulation. In: Design Automation Conference (June 2002)","DOI":"10.1145\/513918.513946"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_4","volume-title":"Formal Methods in Computer-Aided Design","author":"I.-H. Moon","year":"2002","unstructured":"Moon, I.-H., Kwak, H.H., Kukula, J., Shiple, T., Pixley, C.: Simplifying circuits for formal verification using parametric representation. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Chauhan, P., Clarke, E.M., Kroening, D.: A SAT-based algorithm for reparameterization in symbolic simulation. In: Design Automation Conference (June 2004)","DOI":"10.1145\/996566.996711"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/3-540-49519-3_20","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Mador-Haim","year":"1998","unstructured":"Mador-Haim, S., Fix, L.: Input elimination and abstraction in model checking. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 304\u2013320. Springer, Heidelberg (1998)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/3-540-46002-0_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2002","unstructured":"Jin, H., Kuehlmann, A., Somenzi, F.: Fine-grain conjunction scheduling for symbolic reachability analysis. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 312. Springer, Heidelberg (2002)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (2002)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/3-540-44585-4_10","volume-title":"Computer Aided Verification","author":"A. Kuehlmann","year":"2001","unstructured":"Kuehlmann, A., Baumgartner, J.: Transformation-based verification using generalized retiming. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 104. Springer, Heidelberg (2001)"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Wang, D., Ho, P.-H., Long, J., Kukula, J.H., Zhu, Y., Ma, H.-K.T., Damiano, R.F.: Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In: Design Automation Conference (June 2001)","DOI":"10.1145\/378239.378260"},{"key":"18_CR11","unstructured":"Wang, D.: SAT based Abstraction Refinement for Hardware Verification. PhD thesis, Carnegie Mellon University (May 2003)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"van Eijk, C.A.J.: Sequential equivalence checking without state space traversal. In: Design, Automation, and Test in Europe (March 1998)","DOI":"10.1109\/DATE.1998.655922"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on CAD (December 2002)","DOI":"10.1109\/TCAD.2002.804386"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Design Automation Conference (June 2005)","DOI":"10.1145\/1065579.1065700"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and System\u00a016(3) (1994)","DOI":"10.1145\/177492.177725"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Ford, L.R., Fulkerson, D.R.: Maximal flow through a network. Canadian Journal of Mathematics\u00a08 (1956)","DOI":"10.4153\/CJM-1956-045-5"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-48153-2_29","volume-title":"Correct Hardware Design and Verification Methods","author":"K. Fisler","year":"1999","unstructured":"Fisler, K., Vardi, M.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 338\u2013342. Springer, Heidelberg (1999)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_12","volume-title":"Computer Aided Verification","author":"J.H. Kukula","year":"2000","unstructured":"Kukula, J.H., Shiple, T.R.: Building circuits from relations. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-540-30494-4_17","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Awedh","year":"2004","unstructured":"Awedh, M., Somenzi, F.: Increasing the robustness of bounded model checking by computing lower bounds on the reachable states. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 230\u2013244. Springer, Heidelberg (2004)"},{"key":"18_CR20","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. Clarke","year":"2002","unstructured":"Clarke, E., 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, p. 265. Springer, Heidelberg (2002)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-45657-0_12","volume-title":"Computer Aided Verification","author":"J. Baumgartner","year":"2002","unstructured":"Baumgartner, J., Kuehlmann, A., Abraham, J.: Property checking via structural analysis. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 151. Springer, Heidelberg (2002)"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative abstraction using SAT-based BMC with proof analysis. In: Int\u2019l. Conference on Computer-Aided Design (November 2003)","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-540-30494-4_12","volume-title":"Formal Methods in Computer-Aided Design","author":"H. Mony","year":"2004","unstructured":"Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R., Kuehlmann, A.: Scalable automated verification via expert-system guided transformations. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 159\u2013173. Springer, Heidelberg (2004)"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Leiserson, C., Saxe, J.: Retiming synchronous circuitry. Algorithmica\u00a06 (1991)","DOI":"10.1007\/BF01759032"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Heyman, T., Singhal, V., Aziz, A.: An abstraction algorithm for the verification of level-sensitive latch-based netlists. Formal Methods in System Design\u00a0(23) (2003)","DOI":"10.1023\/A:1024485130001"}],"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_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:50:25Z","timestamp":1605642625000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11560548_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}