{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:45Z","timestamp":1760202525351,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028749","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"244-255","source":"Crossref","is-referenced-by-count":28,"title":["BDD based procedures for a theory of equality with uninterpreted functions"],"prefix":"10.1007","author":[{"given":"Anuj","family":"Goel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khurrarn","family":"Sajid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hai","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vigyan","family":"Singhal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"24_CR1","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"W. Ackermann","year":"1954","unstructured":"Wilhelm Ackermann. Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954."},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and Jeremy Levitt. Validity Checking for Combinations of Theories with Equality. In Proc. of the Formal Methods in CAD Conf., November 1996.","DOI":"10.1007\/BFb0031808"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"J. Burch and D. Dill. Automatic Verification of Microprocessor Control. In Proc. of the Computer Aided Verification Conf., July 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"W. Chan, R. Anderson, P. Deame, and D. Notkin. Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Non-linear Constraints. In Proc. of the Computer Aided Verification Conf., July 1997.","DOI":"10.1007\/3-540-63166-6_32"},{"key":"24_CR5","unstructured":"T. H. Cormen, C. E. Leiserson, and R. H. Rivest. Introduction to Algorithms. MIT Press, 1989."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"R. K. Brayton et al. VIS: A system for Verification and Synthesis. In Proc. of the Computer Aided Verification Conf., July 1996.","DOI":"10.1007\/3-540-61474-5_95"},{"key":"24_CR7","unstructured":"M. R. Carey and D. S. Johnson. Computers and Intractability. W. H. Freeman and Co., 1979."},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"R. Hojati, A. Isles, D. Kirkpatrick, and R. Brayton. Verification Using Finite Instantiations and Uninterpreted Functions. In Proc. of the Formal Methods in CAD Conf., November 1996.","DOI":"10.1007\/BFb0031810"},{"key":"24_CR9","unstructured":"R. Hojati, A. Kuehlmann, S. German, and R. Brayton. Validity Checking in the Theory of Equality Using Finite Instantiations. In Proc. Intl. Workshop on Logic Synthesis, May 1997."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Robert B. Jones, David Dill, and Jerry R. Burch. Efficient Validity Checking for Processor Validation. In Proc. Intl. Conf. on Computer-Aided Design, pages 2\u20136, 1995.","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Andreas Kuehlmann and Florian Krolun. Equivalence Checking Using Cuts and Heaps. In Proc. of the Design Automation Conf., June 1997.","DOI":"10.1109\/DAC.1997.597155"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"R. Rudell. Dynamic Variable Ordering for Binary Decision Diagrams. In Proc. Intl. Conf. on Computer-Aided Design, pages 42\u201347, November 1993.","DOI":"10.1109\/ICCAD.1993.580029"},{"issue":"2","key":"24_CR13","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. E. Shostak","year":"1979","unstructured":"R. E. Shostak. A practical decision procedure for arithmetic with function symbols. Journal of the ACM, 26(2):351\u2013360, 1979.","journal-title":"Journal of the ACM"},{"issue":"5","key":"24_CR14","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"Mandayam Srivas and Mark Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52\u201364, September 1990.","journal-title":"IEEE Software"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028749","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T01:45:01Z","timestamp":1736127901000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028749"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0028749","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}