{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:48:55Z","timestamp":1725792535023},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319061993"},{"type":"electronic","value":"9783319062006"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06200-6_17","type":"book-chapter","created":{"date-parts":[[2014,4,23]],"date-time":"2014-04-23T05:53:48Z","timestamp":1398232428000},"page":"215-229","source":"Crossref","is-referenced-by-count":9,"title":["Qed. Computing What Remains to Be Proved"],"prefix":"10.1007","author":[{"given":"Lo\u00efc","family":"Correnson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"17_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.W. Barrett","year":"2005","unstructured":"Barrett, C.W., 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":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: A software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"17_CR3","unstructured":"Baudin, P., Filli\u00e2tre, J.C., Hubert, T., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL Specification Language (2013), http:\/\/frama-c.com\/acsl.html"},{"issue":"1","key":"17_CR4","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1108768.1108813","volume":"31","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. SIGSOFT Softw. Eng. Notes\u00a031(1), 82\u201387 (2005)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"17_CR5","unstructured":"Baudin, P., Correnson, L., Dargaye, Z.: WP User Manual, v0.7 (2013), http:\/\/frama-c.com\/download\/frama-c-wp-manual.pdf"},{"key":"17_CR6","unstructured":"Coq Development Team: The Coq Proof Assistant (2011), http:\/\/coq.inria.fr"},{"key":"17_CR7","unstructured":"Conchon, S., et al.: The Alt-Ergo Automated Theorem Prover, http:\/\/alt-ergo.lri.fr"},{"key":"17_CR8","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Melquiond, G., Paskevich, A.: The Why3 platform 0.81"},{"key":"17_CR9","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/1159876.1159880","volume-title":"Proceedings of the 2006 Workshop on ML 2006","author":"J.C. Filli\u00e2tre","year":"2006","unstructured":"Filli\u00e2tre, J.C., Conchon, S.: Type-safe modular hash-consing. In: Proceedings of the 2006 Workshop on ML 2006, pp. 12\u201319. ACM, New York (2006)"},{"key":"17_CR10","unstructured":"Okasaki, C., Gill, A.: Fast mergeable integer maps. In: Workshop on ML (1998)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Gordon","year":"1996","unstructured":"Gordon, A., Melham, T.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 173\u2013190. Springer, Heidelberg (1996)"},{"key":"17_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/3-540-15975-4_37","volume-title":"Functional Programming Languages and Computer Architecture","author":"T. Johnsson","year":"1985","unstructured":"Johnsson, T.: Lambda lifting: Transforming programs to recursive equations. In: Jouannaud, J.-P. (ed.) Functional Programming Languages and Computer Architecture. LNCS, vol.\u00a0201, pp. 190\u2013203. Springer, Heidelberg (1985)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bjorner, N.: Generalized, efficient array decision procedures. In: IEEE FMCAD, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"17_CR14","unstructured":"Leino, K.R.M.: Efficient weakest preconditions (2003) (unpublished manuscrit), http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml114a.pdf"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06200-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T04:04:34Z","timestamp":1648872274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06200-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319061993","9783319062006"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06200-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}