{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:28Z","timestamp":1755217768007,"version":"3.43.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2003,7]]},"DOI":"10.1023\/a:1024485130001","type":"journal-article","created":{"date-parts":[[2003,9,15]],"date-time":"2003-09-15T13:22:37Z","timestamp":1063632157000},"page":"39-65","source":"Crossref","is-referenced-by-count":8,"title":["An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists"],"prefix":"10.1007","volume":"23","author":[{"given":"Jason","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Tamir","family":"Heyman","sequence":"additional","affiliation":[]},{"given":"Vigyan","family":"Singhal","sequence":"additional","affiliation":[]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5127649_CR1","doi-asserted-by":"crossref","unstructured":"A. Albrecht and A.J. Hu, \u201cRegister transformations with multiple clock domains,\u201d in Proceedings of the Conference on Correct Hardware Design and Verification Methods, Sept. 2001, pp. 126\u2013139.","DOI":"10.1007\/3-540-44798-9_11"},{"key":"5127649_CR2","unstructured":"J. Baumgartner, \u201cAutomatic structural abstraction techniques for enhanced verification,\u201d PhD Thesis, University of Texas at Austin, December 2002."},{"key":"5127649_CR3","doi-asserted-by":"crossref","unstructured":"J. Baumgartner, A. Tripp, A. Aziz, V. Singhal, and F. Andersen, \u201cAn abstraction algorithm for the verification of generalized C-slow designs,\u201d in Proceedings of the Conference on Computer-Aided Verification, July 2000, pp. 5\u201319.","DOI":"10.1007\/10722167_5"},{"key":"5127649_CR4","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh, \u201cThe temporal logic sugar,\u201d in Proceedings of the Conference on Computer-Aided Verification, July 2001, pp. 363\u2013367.","DOI":"10.1007\/3-540-44585-4_33"},{"key":"5127649_CR5","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and A. Landver, \u201cRuleBase: An industry-oriented formal verification tool,\u201d in Proceedings of the Design Automation Conference, June 1996, pp. 655\u2013660.","DOI":"10.1109\/DAC.1996.545656"},{"key":"5127649_CR6","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg, \u201cCharacterizing finite kripke structures in propositional temporal logic,\u201d Theoretical Computer Science, Vol. 59, pp. 115\u2013131, 1988.","journal-title":"Theoretical Computer Science"},{"key":"5127649_CR7","doi-asserted-by":"crossref","first-page":"1057","DOI":"10.1137\/0218072","volume":"18","author":"J. Cheriyan","year":"1989","unstructured":"J. Cheriyan and S.N. Maheshwari, \u201cAnalysis of preflow push algorithms for maximum network flow,\u201d SIAM Journal on Computing, Vol. 18, pp. 1057\u20131086, 1989.","journal-title":"SIAM Journal on Computing"},{"issue":"2","key":"5127649_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla, \u201cAutomatic verification of finite-state concurrent systems using temporal logic specifications,\u201d ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, pp. 244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"5127649_CR9","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern, \u201cSometimes and not never revisited: On branching time versus linear time temporal logic,\u201d Journal of the ACM, Vol. 33, No. 1, pp. 151\u2013178, 1986.","journal-title":"Journal of the ACM"},{"issue":"3","key":"5127649_CR10","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long, \u201cModule checking and modular verification,\u201d ACM Transactions on Programming Languages and Systems, Vol. 16, No. 3, pp. 843\u2013871, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5127649_CR11","doi-asserted-by":"crossref","unstructured":"G. Hasteer, A. Mathur, and P. Banerjee, \u201cEfficient equivalence checking of multi-phase designs using phase abstraction and retiming,\u201d in ACM Transactions on Design Automation of Electronic Systems, October 1998, pp. 600\u2013625.","DOI":"10.1145\/296333.296348"},{"key":"5127649_CR12","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, S. Qadeer, and S.K. Rajamani, \u201cAssume-guarantee refinement between different time scales,\u201d in Proceedings of the Conference on Computer-Aided Verification, July 1999, pp. 208\u2013221.","DOI":"10.1007\/3-540-48683-6_20"},{"key":"5127649_CR13","doi-asserted-by":"crossref","unstructured":"A.J. Hu, G. York, and D.L. Dill, \u201cNew techniques for efficient verification with implicitly conjoined BDDs,\u201d in Proceedings of the Design Automation Conference, June 1994, pp. 276\u2013282.","DOI":"10.1145\/196244.196377"},{"key":"5127649_CR14","doi-asserted-by":"crossref","unstructured":"H. Jin, A. Kuehlmann, and F. Somenzi, \u201cFine-grain conjunction scheduling for symbolic reachability analysis,\u201d in Tools and Algorithms for the Construction and Analysis of Systems, April 2002, pp. 312\u2013326.","DOI":"10.1007\/3-540-46002-0_22"},{"key":"5127649_CR15","unstructured":"Z. Kohavi, Switching and Finite Automata Theory, Computer Science Series, McGraw-Hill Book Company, 1970."},{"key":"5127649_CR16","doi-asserted-by":"crossref","unstructured":"A. Kuehlmann and J. Baumgartner, \u201cTransformation-based verification using generalized retiming,\u201d in Proceedings of the Conference on Computer-Aided Verification, July 2001, pp. 104\u2013117.","DOI":"10.1007\/3-540-44585-4_10"},{"issue":"1","key":"5127649_CR17","first-page":"41","volume":"1","author":"C.E. Leiserson","year":"1983","unstructured":"C.E. Leiserson and J.B. Saxe, \u201cOptimizing synchronous systems,\u201d Journal of VLSI and Computer Systems, Vol. 1, No. 1, pp. 41\u201367, 1983.","journal-title":"Journal of VLSI and Computer Systems"},{"issue":"1","key":"5127649_CR18","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF01759032","volume":"6","author":"C.E. Leiserson","year":"1991","unstructured":"C.E. Leiserson and J.B. Saxe, \u201cRetiming synchronous circuitry,\u201d Algorithmica, Vol. 6, No. 1, pp. 5\u201335, 1991.","journal-title":"Algorithmica"},{"key":"5127649_CR19","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5127649_CR20","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner, Communication and Concurrency, Prentice Hall, New York, 1989."},{"key":"5127649_CR21","doi-asserted-by":"crossref","unstructured":"J.B. Orlin, \u201cA faster strongly polynomial minimum cost flow algorithm,\u201d in Proceedings of the 20th ACM Symposium on the Theory of Computing, May 1988, pp. 377\u2013387.","DOI":"10.1145\/62212.62249"},{"key":"5127649_CR22","unstructured":"R. Rudell, \u201cDynamic variable ordering for ordered binary decision diagrams,\u201d in IEEE\/ACM International Conference on Computer-Aided Design, Nov. 1993, pp. 42\u201347."},{"issue":"1","key":"5127649_CR23","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/43.184852","volume":"12","author":"H. Touati","year":"1993","unstructured":"H. Touati and R. Brayton, \u201cComputing the initial states of retimed circuits,\u201d IEEE Transactions on Computer-Aided Design, Vol. 12, No. 1, pp. 157\u2013162, 1993.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"5127649_CR24","unstructured":"N.Weste, K. Eshraghian, and M.J.S. Smith, Principles of CMOSVLSI Design: A Systems Perspective, Addison Wesley, 2001."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1024485130001.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1024485130001\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1024485130001.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:05:35Z","timestamp":1754420735000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1024485130001"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["5127649"],"URL":"https:\/\/doi.org\/10.1023\/a:1024485130001","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}