{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:49:09Z","timestamp":1725572949703},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540374060"},{"type":"electronic","value":"9783540374114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_42","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T01:07:51Z","timestamp":1154740071000},"page":"467-470","source":"Crossref","is-referenced-by-count":2,"title":["The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover"],"prefix":"10.1007","author":[{"given":"Kenneth","family":"Roe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"42_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: Smt-comp: Satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 20\u201323. Springer, Heidelberg (2005)"},{"key":"42_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11532231_23","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: The mathSAT 3 system. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 315\u2013321. Springer, Heidelberg (2005)"},{"key":"42_CR3","unstructured":"de\u00a0Moura, L.: System description: Yices 0.1. Technical report, Computer Science Laboratory, SRI International, 333 Ravenswood Ave., Menlo Park, CA 94062 (July 2005), \n                    \n                      http:\/\/fm.csl.sri.com\/yices"},{"key":"42_CR4","unstructured":"Dutertre, B., de\u00a0Moura, L.: Simplics: Tool description. Technical report, Computer Science Laboratory, SRI International, 333 Ravenswood Ave., Menlo Park, CA 94062 (July 2005), \n                    \n                      http:\/\/fm.csl.sri.com\/simplics"},{"key":"42_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":"42_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"key":"42_CR7","unstructured":"Ramani, A., Aloul, F.A., Markov, I.L., Sakallah, K.A.: Dynamic symmetry-breaking for improved boolean optimization. In: Asia and South Pacific Design Automation Conference (ASP-DAC) (Januray 2005)"},{"key":"42_CR8","unstructured":"Ranise, S., Tinelli, C.: The smt-lib standard: Version 1.1. Technical report, Department of Computer Science, The University of Iowa (2005), Available at: \n                    \n                      goedel.cs.uiowa.edu\/smtlib"},{"key":"42_CR9","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. 40th Design Automation Conference (DAC), pp. 425\u2013430 (June 2003)","DOI":"10.1145\/775832.775945"},{"key":"42_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S., Bryant, R.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 209. Springer, Heidelberg (2002)"},{"key":"42_CR11","series-title":"Lecture Notes in Computer Science","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., Dill, D.: CVC: a Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 500. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_42.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:30:06Z","timestamp":1619494206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11817963_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}