{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:28:05Z","timestamp":1760783285678},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_12","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T14:42:14Z","timestamp":1277822534000},"page":"159-173","source":"Crossref","is-referenced-by-count":28,"title":["Scalable Automated Verification via Expert-System Guided Transformations"],"prefix":"10.1007","author":[{"given":"Hari","family":"Mony","sequence":"first","affiliation":[]},{"given":"Jason","family":"Baumgartner","sequence":"additional","affiliation":[]},{"given":"Viresh","family":"Paruthi","sequence":"additional","affiliation":[]},{"given":"Robert","family":"Kanzelman","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Kuehlmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Int\u2019l Workshop on Automatic Verification Methods for Finite State Systems (June 1989)","DOI":"10.1007\/3-540-52148-8_30"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a SAT-solver. In: Formal Methods in Computer-Aided Design (November 2000)","DOI":"10.1007\/3-540-40922-X_8"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Tools and Algorithms for Construction and Analysis of Systems (March 1999)","DOI":"10.21236\/ADA360973"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Ganai, M., Aziz, A., Kuehlmann, A.: Enhancing simulation with BDDs and ATPG. In: Design Automation Conference (June 1999)","DOI":"10.1145\/309847.309965"},{"key":"12_CR5","unstructured":"Ho, P.-H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart simulation using collaborative formal and simulation engines. In: Int\u2019l Conference on Computer-Aided Design (November 2000)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Baumgartner, J.: Transformation-based verification using generalized retiming. In: Computer-Aided Verification (July 2001)","DOI":"10.1007\/3-540-44585-4_10"},{"key":"12_CR7","unstructured":"Baumgartner, J.: Automatic Structural Abstraction Techniques for Enhanced Verification. PhD thesis, University of Texas (December 2002)"},{"key":"12_CR8","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"M. Gordon","year":"1989","unstructured":"Gordon, M.: Mechanizing programming logics in higher order logic. In: Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, Heidelberg (1989)"},{"key":"12_CR9","volume-title":"Formal Hardware Verification: Methods and Systems in Comparison","author":"M. Srivas","year":"1997","unstructured":"Srivas, M., Rue\u00df, H., Cyrluk, D.: Hardware verification using PVS. In: Formal Hardware Verification: Methods and Systems in Comparison, Springer, Heidelberg (1997)"},{"key":"12_CR10","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. Handbook of Theoretical Computer Science, vol. B (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"12_CR12","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 Computer-Aided Design\u00a021(12) (2002)","DOI":"10.1109\/TCAD.2002.804386"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Formal Methods in Computer-Aided Design (November 2000)","DOI":"10.1007\/3-540-40922-X_23"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Kuehlmann, A.: Min-area retiming on flexible circuit structures. In: Int\u2019l Conference on Computer-Aided Design (November 2001)","DOI":"10.1109\/ICCAD.2001.968615"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Kuehlmann, A., Abraham, J.: Property checking via structural analysis. In: Computer-Aided Verification (July 2002)","DOI":"10.1007\/3-540-45657-0_12"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Moon, I.-H., Kwak, H.H., Kukula, J., Shiple, T., Pixley, C.: Simplifying circuits for formal verification using parametric representation. In: Formal Methods in Computer-Aided Design (November 2002)","DOI":"10.1007\/3-540-36126-X_4"},{"key":"12_CR17","unstructured":"Wang, D.: SAT based Abstraction Refinement for Hardware Verification. PhD thesis, Carnegie Mellon University (May 2003)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Moon, I.-H., Hachtel, G.D., Somenzi, F.: Border-block triangular form and conjunction schedule in image computation. In: Formal Methods in Computer-Aided Design (November 2000)","DOI":"10.1007\/3-540-40922-X_6"},{"key":"12_CR19","unstructured":"Feigenbaum, E.A.: Themes and case studies of knowledge engineering. In: Expert Systems in the Micro-Electronic Age (1979)"},{"key":"12_CR20","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, (23) (2003)","DOI":"10.1023\/A:1024485130001"},{"key":"12_CR21","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"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:54:59Z","timestamp":1605743699000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}