{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T22:25:48Z","timestamp":1767651948647,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614746"},{"type":"electronic","value":"9783540685999"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_95","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:41:52Z","timestamp":1330292512000},"page":"428-432","source":"Crossref","is-referenced-by-count":245,"title":["VIS: A system for verification and synthesis"],"prefix":"10.1007","author":[{"given":"Robert K.","family":"Brayton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary D.","family":"Hachtel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Szu -Tsung","family":"Cheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Edwards","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sunil","family":"Khatri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuji","family":"Kukimoto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abelardo","family":"Pardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev K.","family":"Ranjan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaker","family":"Sarwary","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas R.","family":"Staple","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gitanjali","family":"Swamy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tiziano","family":"Villa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"43_CR1","doi-asserted-by":"crossref","unstructured":"A. Aziz, S. Tasiran, and R. K. Brayton. BDD Variable Ordering for Interacting Finite State Machines. In Proc. of the Design Automation Conf., pages 283\u2013288, San Diago, CA, June 1994.","DOI":"10.1145\/196244.196379"},{"key":"43_CR2","volume-title":"Technical Report UCB\/ERL M95","author":"R. K. Brayton","year":"1995","unstructured":"R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A System for Verification and Synthesis. Technical Report UCB\/ERL M95, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, Dec. 1995."},{"key":"43_CR3","volume-title":"Technical Report UCB\/ERL M94\/37","author":"S. T. Cheng","year":"1994","unstructured":"S. T. Cheng. Compiling Verilog into Automata. Technical Report UCB\/ERL M94\/37, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, May 1994."},{"key":"43_CR4","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proc. 32nd Design Automat. Conf., pages 427\u2013432, June 1995.","DOI":"10.1145\/217474.217565"},{"key":"43_CR5","unstructured":"S. Edwards. The Ext System, 1995. http:\/\/www.eecs.berkeley.edu\/r~sedwards\/ext."},{"key":"43_CR6","doi-asserted-by":"crossref","unstructured":"H. Fujii, G. Ootomo, and C. Hori. Interleaving based variable ordering methods for ordered binary decision diagrams. In Proc. Intl. Conf. on Computer-Aided Design, pages 38\u201341, Nov. 1993.","DOI":"10.1109\/ICCAD.1993.580028"},{"key":"43_CR7","volume-title":"Technical Report UCB\/ERL M94\/100","author":"R. K. Ranjan","year":"1994","unstructured":"R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton. Efficient Formal Design Verification: Data Structure + Algorithms. Technical Report UCB\/ERL M94\/100, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, Oct. 1994."},{"key":"43_CR8","volume-title":"Technical Report UCB\/ERL M92\/41","author":"E. M. Sentovich","year":"1992","unstructured":"E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. SIS: A System for Sequential Circuit Synthesis. Technical Report UCB\/ERL M92\/41, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, May 1992."},{"key":"43_CR9","unstructured":"The VIS Group. VIS: Verification Interacting with Synthesis, 1995. http:\/\/www-cad.eecs.berkeley.edu\/Respep\/Research\/vis."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_95.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:19:18Z","timestamp":1742599158000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_95"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_95","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}