{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T15:45:32Z","timestamp":1726847132352},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_40","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T16:12:31Z","timestamp":1167408751000},"page":"497-501","source":"Crossref","is-referenced-by-count":6,"title":["System Description: Embedding Verification into Microsoft Excel"],"prefix":"10.1007","author":[{"given":"Graham","family":"Collins","sequence":"first","affiliation":[]},{"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"40_CR1","doi-asserted-by":"crossref","unstructured":"Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The PROSPER Toolkit. In: TACAS 2000 (2000) (to appear)","DOI":"10.1007\/3-540-46419-0_7"},{"volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","year":"1993","key":"40_CR2","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"40_CR3","unstructured":"Hyv\u00f6, E., De Pascale, S.: A New Basis for Spreadsheet Computing: Interval Solver\n                           \n                    TM\n                   forMicrosoft Excel. In: Proceedings of 16th National Conference on Artificial Intelligence and 11th Innovative Applications of Artificial Intelligence Conference (AAAI\/IAAI 1999), pp. 799\u2013806. AAAI Press \/ The MIT Press (1999)"},{"key":"40_CR4","unstructured":"Microsoft Corporation, Microsoft Excel, \n                    \n                      http:\/\/www.microsoft.com\/excel"},{"key":"40_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"1998","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on st\u00e5lmarck\u2019s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 82\u201399. Springer, Heidelberg (1998)"},{"key":"40_CR6","first-page":"31","volume-title":"Proceedings of SAFECOMP 1990","author":"G. St\u00e5lmarck","year":"1990","unstructured":"St\u00e5lmarck, G., S\u00e4flund, M.: Modelling and Verifying Systems and Software in Propositional Logic. In: Proceedings of SAFECOMP 1990, pp. 31\u201336. Pergamon Press, Oxford (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T06:16:31Z","timestamp":1553321791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/10721959_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}