{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:42:02Z","timestamp":1725565322664},"publisher-location":"Berlin, Heidelberg","reference-count":23,"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_13","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:57:57Z","timestamp":1284440277000},"page":"162-174","source":"Crossref","is-referenced-by-count":12,"title":["An Experimental Evaluation of Ground Decision Procedures"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"de Moura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"8","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions in Computers\u00a08, 677\u2013691 (1986)","journal-title":"IEEE Transactions in Computers"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"13_CR3","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)"},{"key":"13_CR4","series-title":"Stump, A., Barrett, C.W., Dill, D.L","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C.W., Dill, D.L.: CVC: a cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. Stump, A., Barrett, C.W., Dill, D.L, vol.\u00a02404, p. 500. Springer, Heidelberg (2002)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 246. Springer, Heidelberg (2001)"},{"key":"13_CR6","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.E. Bryant","year":"2002","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: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 78. Springer, Heidelberg (2002)"},{"key":"13_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 195. Springer, Heidelberg (2002)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Validity checking for combinations of theories with equality","author":"C. Barrett","year":"1996","unstructured":"Barrett, C., Dill, D., Levitt, J.: FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P.J. Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. Journal of the ACM\u00a027, 758\u2013771 (1980)","journal-title":"Journal of the ACM"},{"key":"13_CR10","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01, 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. Journal of the ACM\u00a031, 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45610-4_1","volume-title":"Rewriting Techniques and Applications","author":"N. Shankar","year":"2002","unstructured":"Shankar, N., Rue\u00df, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, p. 1. Springer, Heidelberg (2002)"},{"key":"13_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 438. Springer, Heidelberg (2002)"},{"key":"13_CR14","unstructured":"Ackermann, W.: Solvable cases of the decision problem. Studies in Logic and the Foundation of Mathematics (1954)"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1145\/322276.322288","volume":"28","author":"R.E. Shostak","year":"1981","unstructured":"Shostak, R.E.: Deciding linear inequalities by computing loop residues. Journal of the ACM\u00a028, 769\u2013779 (1981)","journal-title":"Journal of the ACM"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Goel, A., Sajid, K., Zhou, H., Aziz, A.: BDD based procedures for a theory of equality with uninterpreted functions. LNCS , vol.\u00a01427, pp.244\u2013255 (1998)","DOI":"10.1007\/BFb0028749"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: Deciding equality formulas by small domains instantiations. LNCS, vol.\u00a01633, pp. 455\u2013469 (1999)","DOI":"10.1007\/3-540-48683-6_39"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Exploiting positive equality in a logic of equality with uninterpreted functions","author":"R.E. Bryant","year":"1999","unstructured":"Bryant, R.E., German, S., Velev, M.N.: CAV 1999. LNCS, vol.\u00a01633, pp. 470\u2013482. Springer, Heidelberg (1999)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S.A., Bryant, R.E.: Reducing linear inequalities to propositional formulas. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 236. Springer, Heidelberg (2002)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"R. Joshi","year":"2003","unstructured":"Joshi, R., Ou, X., Saxe, J.B., Flanagan, C.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"13_CR22","unstructured":"de Moura, L., Rue\u00df, H., Shankar, N.: Justifying Equality. Submitted for publication (2004), \n                  \n                    http:\/\/www.csl.sri.com\/users\/ruess\/papers\/PDPAR04\/index.html"},{"key":"13_CR23","unstructured":"Ranise, S., Tinelli, C.: The smt-lib format: An initial proposal. In: Proceedings of the 1st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2003), Miami, Florida, pp. 94\u2013111 (2003)"}],"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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T22:18:13Z","timestamp":1558304293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}