{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:32:52Z","timestamp":1740547972231,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223429"},{"type":"electronic","value":"9783540278139"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_34","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:57:57Z","timestamp":1284440277000},"page":"440-452","source":"Crossref","is-referenced-by-count":6,"title":["Efficient Modeling of Embedded Memories in Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Malay K.","family":"Ganai","sequence":"first","affiliation":[]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"Pranav","family":"Ashar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, E.M., Clarke, M.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the Design Automation Conference, pp. 317\u2013320 (1999)","key":"34_CR1","DOI":"10.21236\/ADA360973"},{"doi-asserted-by":"crossref","unstructured":"Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Proceedings of Conference on Formal Methods in Computer-Aided Design (2000)","key":"34_CR2","DOI":"10.1007\/3-540-40922-X_23"},{"unstructured":"Ganai, M., Aziz, A.: Improved SAT-based Bounded Reachability Analysis. In: Proceedings of VLSI Design Conference (2002)","key":"34_CR3"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-46419-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2000","unstructured":"P. A. Abdulla, P. Bjesse, and N. Een, \"Symbolic Reachability Analysis based on {SAT}- Solvers,\" in Proceedings of Workshop on Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 2000."},{"key":"34_CR5","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"34_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"34_CR7","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers\u00a048, 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of Design Automation Conference (2001)","key":"34_CR9","DOI":"10.1145\/378239.379017"},{"doi-asserted-by":"crossref","unstructured":"Ganai, M., Zhang, L., Ashar, P., Gupta, A.: Combining Strengths of Circuit-based and CNF-based Algorithms for a High Performance SAT Solver. In: Proceedings of the Design Automation Conference (2002)","key":"34_CR10","DOI":"10.1145\/513918.514105"},{"doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Ganai, M., Paruthi, V.: Circuit-based Boolean Reasoning. In: Proceedings of Design Automation Conference (2001)","key":"34_CR11","DOI":"10.1145\/378239.378470"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"unstructured":"Long, D.E.: Model checking, abstraction and compositional verification. Carnegie Mellon University (1993)","key":"34_CR13"},{"key":"34_CR14","volume-title":"Computer-Aided Verification of Co-ordinating Processes: The Automata- Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Co-ordinating Processes: The Automata- Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"34_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"34_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45657-0_20","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 265. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Wang, D., Ho, P.-H., Long, J., Kukula, J., Zhu, Y., Ma, T., Damiano, R.: Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines. In: 38th Design Automation Conference (2001)","key":"34_CR17","DOI":"10.1145\/378239.378260"},{"doi-asserted-by":"crossref","unstructured":"Chauhan, P., Clarke, E.M., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis. In: Proceedings of FMCAD (2002)","key":"34_CR18","DOI":"10.1007\/3-540-36126-X_3"},{"doi-asserted-by":"crossref","unstructured":"McMillan, K., Amla, N.: Automatic Abstraction without Counterexamples. In: Tools and Algorithms for the Construction and Analysis of Systems (April 2003)","key":"34_CR19","DOI":"10.1007\/3-540-36577-X_2"},{"unstructured":"Gupta, M., Ganai, P.: Iterative Abstraction using SAT-based BMC with Proof Analysis. In: Proceedings of International Conference on Computer-Aided Design (2003)","key":"34_CR20"},{"doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E., Jain, A.: Efficient Modeling of Memory Arrays in Symbolic Simulation. In: Grumberg, O. (ed.) Computer Aided Verification, pp. 388\u2013399 (1997)","key":"34_CR21","DOI":"10.1007\/3-540-63166-6_38"},{"key":"34_CR22","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Computer-Aided Verification","author":"R.E. Bryant","year":"1999","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic. In: Halbwachs, N., Peled, D. (eds.) Computer-Aided Verification, pp. 470\u2013482. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, pp. 252\u2013267 (2001)","key":"34_CR23","DOI":"10.1007\/3-540-45319-9_18"},{"doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and Verification of Out-of-Order Microprocessors in UCLID. In: Proceedings of Formal Methods in Computer-Aided Design, pp. 142\u2013159 (2002)","key":"34_CR24","DOI":"10.1007\/3-540-36126-X_9"},{"doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Computer-Aided Verification (2002)","key":"34_CR25","DOI":"10.1007\/3-540-45657-0_7"},{"key":"34_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, E.M.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking Safety Properties using Induction and a SAT Solver. In: Proceedings of Conference on Formal Methods in Computer-Aided Design (2000)","key":"34_CR27","DOI":"10.1007\/3-540-40922-X_8"},{"doi-asserted-by":"crossref","unstructured":"Pilarski, S., Hu, G.: Speeding up SAT for EDA. In: Proceedings of Design Automation and Test in Europe, p. 1081 (2002)","key":"34_CR28","DOI":"10.1109\/DATE.2002.998437"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T19:48:25Z","timestamp":1740512905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}