{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:08:06Z","timestamp":1746158886942},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_54","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T18:29:34Z","timestamp":1188412174000},"page":"547-560","source":"Crossref","is-referenced-by-count":29,"title":["A Lazy and Layered SMT( $\\mathcal{BV}$ ) Solver for Hard Industrial Verification Problems"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Bruttomesso","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"Franz\u00e9n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ziyad","family":"Hanna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Nadel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amit","family":"Palti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"54_CR1","unstructured":"http:\/\/mathsat.itc.it\/cav07-bitvectors\/"},{"key":"54_CR2","volume-title":"Proc. DAC 2004","author":"Z.S. Andraus","year":"2004","unstructured":"Andraus, Z.S., Sakallah, K.A.: Automatic abstraction and verification of verilog models. In: Proc. DAC 2004, ACM Press, New York (2004)"},{"key":"54_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: A Decision Procedure for Bit-Vector Arithmetic. In: Design Automation Conference, pp. 522\u2013527 (1998)","DOI":"10.21236\/ADA400400"},{"key":"54_CR4","series-title":"ENTCS","volume-title":"Proc. PDPAR 2005","author":"M. Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Hanna, Z., Khasidashvili, Z., Palti, A., Sebastiani, R.: Encoding RTL Constructs for MathSAT: a Preliminary Report. In: Proc. PDPAR 2005. ENTCS, vol.\u00a0144 (2), Elsevier, Amsterdam (2006)"},{"key":"54_CR5","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: MathSAT: A Tight Integration of SAT and Mathematical Decision Procedure. Journal of Automated Reasoning\u00a035(1-3) (2005)","DOI":"10.1007\/s10817-005-9004-z"},{"key":"54_CR6","first-page":"741","volume-title":"Proc. ASP-DAC 2002","author":"R. Brinkmann","year":"2002","unstructured":"Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proc. ASP-DAC 2002, pp. 741\u2013746. IEEE Computer Society Press, Los Alamitos (2002)"},{"issue":"8","key":"54_CR7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a0C35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"54_CR8","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J.W. Chinneck","year":"1991","unstructured":"Chinneck, J.W., Dravnieks, E.W.: Locating Minimal Infeasible Constraint Sets in Linear Programs. ORSA Journal on Computing\u00a03(2), 157\u2013168 (1991)","journal-title":"ORSA Journal on Computing"},{"key":"54_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"D. Cyrluk","year":"1997","unstructured":"Cyrluk, D., M\u00f6ller, O., Rue\u00df, H.: An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"54_CR10","unstructured":"Dutertre, B., de Moura, L.: System Description: Yices 1.0. In: Proc. SMT-COMP 2006 (2006)"},{"key":"54_CR11","unstructured":"Ganesh, V., Berezin, S., Dill, D.L.: A Decision Procedure for Fixed-width Bit-vectors. Technical report, Stanford University (2005), http:\/\/theory.stanford.edu\/~vganesh\/"},{"key":"54_CR12","doi-asserted-by":"crossref","unstructured":"Johannsen, P., Drechsler, R.: Speeding Up Verification of RTL Designs by Computing One-to-one Abstractions with Reduced Signal Widths. In: VLSI-SOC (2001)","DOI":"10.1007\/978-0-387-35597-9_31"},{"key":"54_CR13","volume-title":"Proc. ICCAD 2006","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Srinivasan, S.K., Vroon, D.: Automatic Memory Reductions for RTL-Level Verification. In: Proc. ICCAD 2006, ACM Press, New York (2006)"},{"key":"54_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-49254-2","volume-title":"Formal Methods in Computer-Aided Design","author":"M.O. M\u00f6ller","year":"1998","unstructured":"M\u00f6ller, M.O., Ruess, H.: Solving bit-vector equations. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, Springer, Heidelberg (1998)"},{"key":"54_CR15","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhang, Y.Z.L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (2001)","DOI":"10.1145\/378239.379017"},{"key":"54_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44881-0","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2003","unstructured":"Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, Springer, Heidelberg (2003)"},{"key":"54_CR17","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions. In: Proc. DAC 2003 (2003)","DOI":"10.1145\/775832.775945"},{"key":"54_CR18","series-title":"ENTCS","volume-title":"Proc. PDPAR 2005","author":"E. Singerman","year":"2006","unstructured":"Singerman, E.: Challenges in making decision procedures applicable to industry. In: Proc. PDPAR 2005. ENTCS, vol.\u00a0144 (2), Elsevier, Amsterdam (2006)"},{"key":"54_CR19","volume-title":"Proc. DATE 2001","author":"Z. Zeng","year":"2001","unstructured":"Zeng, Z., Kalla, P., Ciesielski, M.: LPSAT: a unified approach to RTL satisfiability. In: Proc. DATE 2001, IEEE Computer Society Press, Los Alamitos (2001)"}],"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-73368-3_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:08:40Z","timestamp":1619503720000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_54","relation":{},"subject":[]}}