{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:55:49Z","timestamp":1725551749913},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540297970"},{"type":"electronic","value":"9783540322504"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11576280_23","type":"book-chapter","created":{"date-parts":[[2005,10,24]],"date-time":"2005-10-24T14:01:26Z","timestamp":1130162486000},"page":"330-344","source":"Crossref","is-referenced-by-count":4,"title":["Using St\u00e5lmarck\u2019s Algorithm to Prove Inequalities"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Georges","family":"Gonthier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Andersson, G., Bjesse, P., Cook, B., Hanna, Z.: A proof engine approach to solving combinational design automation problems. In: 2002 Design Automation Conference (2002)","key":"23_CR1","DOI":"10.1109\/DAC.2002.1012718"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-540-24730-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Das, S., Rajamani, S.K.: Refining approximations in software predicate abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 388\u2013403. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: CAV 2004: International Conference on Computer-Aided Verification (2004)","key":"23_CR3","DOI":"10.1007\/978-3-540-27813-9_36"},{"doi-asserted-by":"crossref","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Cogent: Accurate theorem proving for program verification. To appear at CAV 05: Conference on Computer Aided Verification (2005)","key":"23_CR4","DOI":"10.1007\/11513988_30"},{"key":"23_CR5","volume-title":"Introduction to Lattices and Order","author":"B.A. Davey","year":"1990","unstructured":"Davey, B.A., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV 1997: Conference on Computer Aided Verification (1997)","key":"23_CR6","DOI":"10.1007\/3-540-63166-6_10"},{"doi-asserted-by":"crossref","unstructured":"Harrison, J.: St\u00e5lmarck\u2019s method as a HOL derived rule. In: TPHOLs 1996: International Conference on Theorem Proving in Higher Order Logics (1996)","key":"23_CR7","DOI":"10.1007\/BFb0105407"},{"doi-asserted-by":"crossref","unstructured":"Kunz, W., Pradhan, D.K.: Recursive learning: An attractive alternative to the decision tree for test generation in digital circuits. In: ITC 1992: International Test Conference (1992)","key":"23_CR8","DOI":"10.1109\/TEST.1992.527905"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/11513988_5","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2005","unstructured":"Lahiri, S.K., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 24\u201338. Springer, Heidelberg (2005)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"unstructured":"Microsoft Corporation. Static Driver Verifier, Available at http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/SDV.mspx","key":"23_CR11"},{"unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. Formal Methods in System Design\u00a016(1) (January 000)","key":"23_CR12"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11576280_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:59:34Z","timestamp":1605643174000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11576280_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297970","9783540322504"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/11576280_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}