{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T17:46:36Z","timestamp":1793036796435,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439974","type":"print"},{"value":"9783540456575","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_18","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"236-249","source":"Crossref","is-referenced-by-count":74,"title":["Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT"],"prefix":"10.1007","author":[{"given":"Clark W.","family":"Barrett","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and J. Levitt. Validity Checking for Combinations of Theories with Equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods In Computer-Aided Design, pages 187\u2013201, 1996.","DOI":"10.1007\/BFb0031808"},{"key":"18_CR2","unstructured":"Clark W. Barrett. Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories. PhD thesis, Stanford University, 2002."},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"R. Bryant, S. German, and M. Velev. Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. In 11th International Conference on Computer-Aided Verification, pages 470\u2013482, 1999.","DOI":"10.1007\/3-540-48683-6_40"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura, Harald Ruess, and Maria Sorea. Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. In 18th International Conference on Automated Deduction, 2002.","DOI":"10.1007\/3-540-45620-1_35"},{"key":"18_CR5","unstructured":"L. e Silva, L. Silveira, and J. Marques-Silva. Algorithms for Solving Boolean Satisfiability in Combinational Circuits. In Proceedings of the IEEE\/ACM Design, Automation and Test in Europe Conference (DATE), March 1999."},{"key":"18_CR6","unstructured":"C. Flanagan. Private Communication, 2000."},{"key":"18_CR7","unstructured":"Cormac Flanagan, Rajeev Joshi, and James B. Saxe. The Design of An Efficient Theorem Prover using Explicated Clauses. 2002. In Preparation."},{"issue":"1","key":"18_CR8","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"Tracy Larrabee","year":"1992","unstructured":"Tracy Larrabee. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design, 11(1):4\u201315, January 1992.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"18_CR9","unstructured":"Jeremy R. Levitt. Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University, 1999."},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 39th Design Automation Conference, 2001.","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"18_CR11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u201357, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding Equality Formulas by Small-Domain Instantiations. In 11th International Conference on Computer-Aided Verification, pages 455\u2013469, 1999.","DOI":"10.1007\/3-540-48683-6_39"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"H. Ruess and N. Shankar. Deconstructing Shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19\u201328, June 2001.","DOI":"10.1109\/LICS.2001.932479"},{"key":"18_CR14","unstructured":"Laurent Simon. The Sat-Ex Site. \n                    http:\/\/www.lri.fr\/~simon\/satex\/satex.php3\n                    \n                  ."},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"A. Stump, C. Barrett, and D. Dill. CVC: a Cooperating Validity Checker. In 14th International Conference on Computer-Aided Verification, 2002.","DOI":"10.1007\/3-540-45657-0_40"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T20:04:50Z","timestamp":1550347490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}