{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:16:54Z","timestamp":1725560214377},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_19","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T14:56:52Z","timestamp":1279724212000},"page":"255-259","source":"Crossref","is-referenced-by-count":0,"title":["Decision Procedures Customized for Formal Verification"],"prefix":"10.1007","author":[{"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","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.G., 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, pp. 195\u2013210. Springer, Heidelberg (2002)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"1999","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 470\u2013482. Springer, Heidelberg (1999)"},{"issue":"1","key":"19_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/371282.371364","volume":"2","author":"R.E. Bryant","year":"2001","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic\u00a02(1), 1\u201341 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"19_CR4","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, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/10722167_10","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2000","unstructured":"Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 85\u201398. Springer, Heidelberg (2000)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Transactions on Computational Logic\u00a03(4) (October 2002)","DOI":"10.1145\/566385.566390"},{"key":"19_CR7","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, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-27813-9_40","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 475\u2013478. Springer, Heidelberg (2004)"},{"key":"19_CR9","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1992","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1992)"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: 38th Design Automation Conference (DAC 2001), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"19_CR11","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(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR12","unstructured":"Seshia, S.A.: Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification. PhD thesis, Carnegie Mellon University (2005)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Bryant, R.E.: Deciding quantifier-free Presburger formulas using parameterized solution bounds. In: 19\n                  th\n                 IEEE Symposium on Logic in Computer Science (LICS) (July 2004)","DOI":"10.1109\/LICS.2004.1319604"},{"key":"19_CR14","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: 40th Design Automation Conference (DAC 2003), pp. 425\u2013430 (June 2003)","DOI":"10.1145\/775832.775945"},{"key":"19_CR15","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.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 500\u2013504. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:09:08Z","timestamp":1605625748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11532231_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}