{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T13:59:13Z","timestamp":1777125553775,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540894384","type":"print"},{"value":"9783540894391","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-89439-1_25","type":"book-chapter","created":{"date-parts":[[2008,11,15]],"date-time":"2008-11-15T03:03:10Z","timestamp":1226718190000},"page":"343-352","source":"Crossref","is-referenced-by-count":20,"title":["Reveal: A Formal Verification Tool for Verilog Designs"],"prefix":"10.1007","author":[{"given":"Zaher S.","family":"Andraus","sequence":"first","affiliation":[]},{"given":"Mark H.","family":"Liffiton","sequence":"additional","affiliation":[]},{"given":"Karem A.","family":"Sakallah","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Andraus, Z., Liffiton, M., Sakallah, K.: Refinement strategies for verification methods based on datapath abstraction. In: Proc. of Asia and South Pacific Design Automation Conference, pp. 19\u201324 (2006)","DOI":"10.1145\/1118299.1118306"},{"key":"25_CR2","unstructured":"Andraus, Z., Liffiton, M., Sakallah, K.: CEGAR-based formal hardware verification: a case study. Technical Report CSE-TR-531-07, University of Michigan (2007)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Andraus, Z., Sakallah, K.: Automatic abstraction and verification of Verilog models. In: Proc. of Design Automation Conference, pp. 218\u2013223 (2004)","DOI":"10.1145\/996566.996629"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R. Bryant","year":"2002","unstructured":"Bryant, R., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with Lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J. Burch","year":"1994","unstructured":"Burch, J., Dill, D.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"issue":"5","key":"25_CR6","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Sixth Annual ACM SI PLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238\u2013252 (2006)","DOI":"10.1145\/512950.512973"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.: Successive approximation of abstract transition relations. In: IEEE Symposium on Logic in Computer Science, pp. 51\u201358 (2001)","DOI":"10.1109\/LICS.2001.932482"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R. Brayton","year":"1996","unstructured":"Brayton, R., et al.: VIS: a system for verfication and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"25_CR11","volume-title":"Computer Architecture: A Quantitative Approach","author":"J. Hensessy","year":"1996","unstructured":"Hensessy, J., Patterson, D.: Computer Architecture: A Quantitative Approach, 2nd edn. Morgan Kaufmann, San Francisco (1996)","edition":"2"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Jain, H., Kroening, D., Sharygina, N., Clarke, E.: Word-level predicate abstraction and refinement for verifying RTL Verilog. In: Proc. of Design Automation Conference, pp. 445\u2013450 (2005)","DOI":"10.21236\/ADA470547"},{"key":"25_CR13","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoritic Approach","author":"R. Kurshan","year":"1999","unstructured":"Kurshan, R.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoritic Approach. Princeton University Press, Princeton (1999)"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S., Vroon, D.: Automatic memory reductions for rtl model verification. In: Proc. of Int\u2019l. Conference on Computer-Aided Design, pp. 786\u2013793 (2006)","DOI":"10.1109\/ICCAD.2006.320121"},{"key":"25_CR15","unstructured":"Wang, F., Li, B., Jin, H., Hachtel, G., Somenzi, F.: Improving Ariadne\u2019s Bundle by following multiple threads in abstraction refinement. In: Proc. of Int\u2019l. Conference on Computer-Aided Design, pp. 408\u2013415 (2003)"},{"key":"25_CR16","unstructured":"http:\/\/yices.csl.sri.com\/"},{"key":"25_CR17","unstructured":"http:\/\/www.eecs.umich.edu\/vips\/stresstest.html"},{"key":"25_CR18","unstructured":"http:\/\/vlsi.cs.iitm.ernet.in\/x86_proj\/x86Homepage.html"},{"key":"25_CR19","unstructured":"http:\/\/www.opencores.org"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89439-1_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,2]],"date-time":"2025-02-02T19:50:48Z","timestamp":1738525848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89439-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540894384","9783540894391"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89439-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}