{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:20:52Z","timestamp":1747592452093},"publisher-location":"Berlin, Heidelberg","reference-count":21,"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_21","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"269-284","source":"Crossref","is-referenced-by-count":5,"title":["Exploiting Constraints in Transformation-Based Verification"],"prefix":"10.1007","author":[{"given":"Hari","family":"Mony","sequence":"first","affiliation":[]},{"given":"Jason","family":"Baumgartner","sequence":"additional","affiliation":[]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Pixley, C.: Integrating model checking into the semiconductor design flow. Electronic Systems Technology & Design (1999)"},{"key":"21_CR2","unstructured":"Accelera. PSL LRM, http:\/\/www.eda.org\/vfv"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028768","volume-title":"Computer Aided Verification","author":"M. Kaufmann","year":"1998","unstructured":"Kaufmann, M., Martin, A., Pixley, C.: Design constraints in symbolic model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Hollander, Y., Morley, M., Noy, A.: The e language: A fresh separation of concerns. In: Technology of Object-Oriented Languages and Systems (2001)","DOI":"10.1109\/TOOLS.2001.911754"},{"key":"21_CR5","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":"21_CR6","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":"21_CR7","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":"21_CR8","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":"21_CR9","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":"21_CR10","doi-asserted-by":"crossref","unstructured":"Yuan, J., Shultz, K., Pixley, C., Miller, H., Aziz, A.: Modeling design constraints and biasing in simulation using BDDs. In: ICCAD (1999)","DOI":"10.1109\/ICCAD.1999.810715"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Yuan, J., Albin, K., Aziz, A., Pixley, C.: Constraint synthesis for environment modeling in functional verification. In: Design Automation Conference (2003)","DOI":"10.1145\/775832.775909"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Design Automation Conference (2005)","DOI":"10.1145\/1065579.1065700"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Leiserson, C., Saxe, J.: Retiming synchronous circuitry. Algorithmica\u00a06 (1991)","DOI":"10.1007\/BF01759032"},{"key":"21_CR14","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":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/11560548_18","volume-title":"Correct Hardware Design and Verification Methods","author":"J. Baumgartner","year":"2005","unstructured":"Baumgartner, J., Mony, H.: Maximal input reduction of sequential netlists via synergistic reparameterization and localization strategies. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 222\u2013237. Springer, Heidelberg (2005)"},{"key":"21_CR16","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"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_5","volume-title":"Computer Aided Verification","author":"J. Baumgartner","year":"2000","unstructured":"Baumgartner, J., Tripp, A., Aziz, A., Singhal, V., Andersen, F.: An abstraction algorithm for the verification of generalized C-slow designs. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"21_CR18","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":"21_CR19","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":"21_CR20","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Kukula, J.: Using counter example guided abstraction refinement to find complex bugs. In: Design Automation and Test in Europe (2004)","DOI":"10.1109\/DATE.2004.1268842"},{"key":"21_CR21","unstructured":"IBM Formal Verification Benchmark Library, http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage\/fvbenchmarks.html"}],"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_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:50:26Z","timestamp":1605642626000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11560548_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}