{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:47:53Z","timestamp":1725551273128},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_1","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:55:19Z","timestamp":1269885319000},"page":"1-18","source":"Crossref","is-referenced-by-count":11,"title":["Abstraction by Symbolic Indexing Transformations"],"prefix":"10.1007","author":[{"given":"Thomas F.","family":"Melham","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert B.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.J.H. Seger","year":"1995","unstructured":"Seger, C.J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design 6 (1995) 147\u2013189","journal-title":"Formal Methods in System Design"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/103516.103519","volume":"38","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E.: A methodology for hardware verification based on logic simulation. Journal of the ACM 38 (1991) 299\u2013328","journal-title":"Journal of the ACM"},{"key":"1_CR3","unstructured":"Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. In: ACM\/IEEE Design Automation Conference, ACM Press (1997) 167\u2013172"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Beatty, D.L., Seger, C.J.H.: Formal hardware verification by symbolic ternary trajectory evaluation. In: ACM\/IEEE Design Automation Conference, ACM Press (1991) 397\u2013402","DOI":"10.1145\/127601.127701"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35 (1986) 677\u2013691","journal-title":"IEEE Transactions on Computers"},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-48683-6_19","volume-title":"Computer Aided Verification (CAV)","author":"C.T. Chou","year":"1999","unstructured":"Chou, C.T.: The mathematical foundation of symbolic trajectory evaluation. In Halbwachs, N., Peled, D., eds.: Computer Aided Verification (CAV). Volume 1633 of Lecture Notes in Computer Science., Springer-Verlag (1999) 196\u2013207"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"1005","DOI":"10.1109\/43.298036","volume":"13","author":"P. Jain","year":"1994","unstructured":"Jain, P., Gopalakrishnan, G.: Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. IEEE Transactions on Computer-Aided Design of Integrated Circuits 13 (1994) 1005\u20131015","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits"},{"key":"1_CR8","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Formal verification using parametric representations of Boolean constraints. In: ACM\/IEEE Design Automation Conference, ACM Press (1999) 402\u2013407"},{"key":"1_CR9","unstructured":"Jones, R.B.: Applications of Symbolic Simulation to the Formal Verification of Microprocessors. PhD thesis, Department of Electrical Engineering, Stanford University (1999)"},{"key":"1_CR10","unstructured":"O\u2019Leary, J.W., Zhao, X., Gerth, R., Seger, C.J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technical Journal (First quarter, 1999) Available at \n                    http:\/\/www.developer.intel.com\/technology\/itj\/\n                    \n                  ."},{"key":"1_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-44659-1_21","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Kaivola","year":"2000","unstructured":"Kaivola, R., Aagaard, M.D.: Divider circuit verification with model checking and theorem proving. In Aagaard, M., Harrison, J., eds.: Theorem Proving in Higher Order Logics. Volume 1869 of Lecture Notes in Computer Science., Springer-Verlag (2000) 338\u2013355"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Combining theorem proving and trajectory evaluation in an industrial environment. In: ACM\/IEEE Design Automation Conference, ACM Press (1998) 538\u2013541","DOI":"10.1145\/277044.277189"},{"key":"1_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"Computer Aided Verification (CAV)","author":"P. Bjesse","year":"2001","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In Berry, G., Comon, H., Finkel, A., eds.: Computer Aided Verification (CAV). Volume 2102 of Lecture Notes in Computer Science., Springer-Verlag (2001) 454\u2013464"},{"key":"1_CR14","unstructured":"Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. In: Proceedings of 2001 IEEE International Conference on Computer Design. (2001) 360\u2013365"}],"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\/3-540-36126-X_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T09:25:09Z","timestamp":1550309109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}