{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:26:06Z","timestamp":1725456366660},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028750","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"256-267","source":"Crossref","is-referenced-by-count":7,"title":["Computing reachable control states of systems modeled with uninterpreted functions and infinite memory"],"prefix":"10.1007","author":[{"given":"Adrian J.","family":"Isles","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramin","family":"Hojati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"issue":"8","key":"25_CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph Based Algorithms for Boolean Function Manipulation\u201d, IEEE Trans. on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Trans. on Computers"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Jerry R. Burch, E. M. Clarke, K. L. McMillan, David L. Dill, \u201cSequential Circus Verification Using Symbolic Model Checking\u201d, Proc. Of the Design Automation Conf., 1990","DOI":"10.1145\/123186.123223"},{"key":"25_CR3","volume-title":"Automatic Verification of Pipelined Microprocessor Control","author":"J. R. Burch","year":"1994","unstructured":"Jerry R. Burch, David L. Dill, \u201cAutomatic Verification of Pipelined Microprocessor Control\u201d, Computer Aided Verification, Stanford, CA, June 1994."},{"issue":"1","key":"25_CR4","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/12.250616","volume":"43","author":"F. Corella","year":"1994","unstructured":"F. Corella, \u201cAutomatic Verification of Behavioral Equivalence for Microprocessors\u201d IEEE Transactions on Computers, 43(1):115\u2013117, January 1994.","journal-title":"IEEE Transactions on Computers"},{"key":"25_CR5","unstructured":"F. Corella, Z. Zhou, X. Song, M. Langevin, E. Cerny, \u201cMultiway Decision Graphs for Automated Hardware Verification\u201d, IBM technical report RC19676, July 1994."},{"key":"25_CR6","unstructured":"K. Fisler and S. Johnson, \u201cIntegrating Design and Verification Environments throug a Logic Supporting Hardware Designs\u201d, Proc. IFIP Conference on Hardware Description Languages and their Applications, Chiba, Japan, Aug. 1995."},{"key":"25_CR7","unstructured":"John L. Hennessy, David A. Patterson, \u201cComputer Architecture A Quantitative Approach\u201d, Morgan Kaufmann Publishers, 1990."},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Ramin Hojati, Robert K. Brayton, \u201cAutomatic Datapath Abstraction of Hardware Systems\u201d, Conference on Computer-Aided Verification, June 1995.","DOI":"10.1007\/3-540-60045-0_43"},{"key":"25_CR9","unstructured":"Ramin Hojati, Adrian J. Isles, and Robert K. Brayton, \u201cAutomatic State Reduction Techniques for Hardware Systems Modeled Using Uninterpreted Functions and Infinite Memory\u201d, IEEE International High Level Design Validation and Test Workshop, Nov 1997."},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Ramin Hojati, Adrian J. Isles, Desmond Kirkpatrick, and Robert K. Brayton, \u201cVerification Using Uninterpreted Functions and Finite Instantiations\u201d, Formal Methods in CAD, November 1996.","DOI":"10.1007\/BFb0031810"},{"key":"25_CR11","unstructured":"W. A. Hunt, Jr. \u201cFM8501: A verified microprocessor\u201d, Technical Report 47, University of Texas at Austin, Institute for Computer Science, Dec. 1985."},{"key":"25_CR12","unstructured":"Adrian J. Isles, Ramin Hojati, and Robert K. Brayton, \u201cReachability Analysis of ICS Models\u201d, SRC Techcon, September 1996."},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"R.B Jones, D. L. Dill and J. R. Burch, \u201cEfficient Validity Checking for Processor Verification\u201d, IEEEIACM International Conference of Computer Aided Design, 1995","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"M. Langevin, E. Cerny, \u201cComparing Generic State Machines\u201d, Computer Aided Verification, July, 1991.","DOI":"10.1007\/3-540-55179-4_43"},{"issue":"2","key":"25_CR15","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Greg Nelson, Derek C. Oppen, \u201cFast Decision Procedures Based on Congruence Closure\u201d, Journal of the ACM, 27(2):356\u2013364, April 1980, June 1995.","journal-title":"Journal of the ACM"},{"issue":"2","key":"25_CR16","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. E. Shostak","year":"1979","unstructured":"R. E. Shostak, \u201cA Practical Decision Procedure for Arithmetic With Function Symbols\u201d, JACM Volume 26, No. 2, April 1979, pp. 351\u2013360.","journal-title":"JACM"},{"key":"25_CR17","unstructured":"F. Somenzi, \u201cCUDD: CU Decision Diagram Package, Release 2.1.1\u201d, Departmen ECE, University of Colorado at Boulder, February 1997."},{"issue":"5","key":"25_CR18","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"M. Srivas and M. Bickford. \u201cFormal Verification of a Pipelined Microprocessor\u201d. IEEE Software, 7(5):52\u201364, Sept 1990.","journal-title":"IEEE Software"},{"key":"25_CR19","unstructured":"The VIS Group, \u201cVIS: A system for Verification and Synthesis\u201d, Conference on Computer Aided Verification, July 1996."},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella, M. Langevin, \u201cFormal Verification of the Island Tunnel Controller Using Multiway Decision Graphs\u201d, Formal Methods in Computer-Aided Design, November 1996.","DOI":"10.1007\/BFb0031811"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028750","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:23:38Z","timestamp":1586593418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028750"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0028750","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}