{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T09:08:58Z","timestamp":1746522538175,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642157684"},{"type":"electronic","value":"9783642157691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_21","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T06:09:40Z","timestamp":1284358180000},"page":"340-355","source":"Crossref","is-referenced-by-count":10,"title":["Verifying a Local Generic Solver in Coq"],"prefix":"10.1007","author":[{"given":"Martin","family":"Hofmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksandr","family":"Karbyshev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Backes, M., Laud, P.: Computationally sound secrecy proofs by mechanized flow analysis. In: ACM Conference on Computer and Communications Security, pp. 370\u2013379 (2006)","DOI":"10.1145\/1180405.1180450"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-24725-8_27","volume-title":"Programming Languages and Systems","author":"D. Cachera","year":"2004","unstructured":"Cachera, D., Jensen, T.P., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 385\u2013400. Springer, Heidelberg (2004)"},{"key":"21_CR3","unstructured":"Le Charlier, B., Van Hentenryck, P.: A universal top-down fixpoint algorithm. Technical Report CS-92-25, Brown University, Providence, RI 02912 (1992)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11617990_8","volume-title":"Types for Proofs and Programs","author":"S. Coupet-Grimal","year":"2006","unstructured":"Coupet-Grimal, S., Delobel, W.: A uniform and certified approach for two static analyses. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/3-540-60360-3_53","volume-title":"Static Analysis","author":"C. Fecht","year":"1995","unstructured":"Fecht, C.: Gena - a tool for generating prolog analyzers from specifications. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983, pp. 418\u2013419. Springer, Heidelberg (1995)"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/BFb0053565","volume-title":"Programming Languages and Systems","author":"C. Fecht","year":"1998","unstructured":"Fecht, C., Seidl, H.: Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol.\u00a01381, pp. 90\u2013104. Springer, Heidelberg (1998)"},{"issue":"2","key":"21_CR7","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0167-6423(99)00009-X","volume":"35","author":"C. Fecht","year":"1999","unstructured":"Fecht, C., Seidl, H.: A faster solver for general systems of equations. Sci. Comput. Program.\u00a035(2), 137\u2013161 (1999)","journal-title":"Sci. Comput. Program."},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-642-14162-1_17","volume-title":"ICALP 2010","author":"M. Hofmann","year":"2010","unstructured":"Hofmann, M., Karbyshev, A., Seidl, H.: What is a pure functional? In: Abramsky, S., Gavoille, C., Kirchner, C., der Heide, F.M.a., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol.\u00a06199, pp. 199\u2013210. Springer, Heidelberg (2010), \n                  \n                    http:\/\/dx.doi.org\/10.1007\/978-3-642-14162-1_17"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78663-4_1","volume-title":"Trustworthy Global Computing","author":"M. Hofmann","year":"2008","unstructured":"Hofmann, M., Pavlova, M.: Elimination of ghost variables in program logics. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol.\u00a04912, pp. 1\u201320. Springer, Heidelberg (2008)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/3-540-58485-4_50","volume-title":"Static Analysis","author":"N. Jorgensen","year":"1994","unstructured":"Jorgensen, N.: Finding fixpoints in finite function spaces using neededness analysis and chaotic iteration. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol.\u00a0864, pp. 329\u2013345. Springer, Heidelberg (1994)"},{"issue":"298","key":"21_CR11","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"3","author":"G. Klein","year":"2003","unstructured":"Klein, G., Nipkow, T.: Verified bytecode verifiers. Theor. Comput. Sci.\u00a03(298), 583\u2013626 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR12","unstructured":"The Coq development team. The Coq proof assistant reference manual. TypiCal Project (formerly LogiCal), Version 8.2-bugfix (2009)"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45315-6_23","volume-title":"Foundations of Software Science and Computation Structures","author":"T. Nipkow","year":"2001","unstructured":"Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 347\u2013363. Springer, Heidelberg (2001)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-03237-0_13","volume-title":"Static Analysis","author":"H. Seidl","year":"2009","unstructured":"Seidl, H., Vojdani, V.: Region analysis for race detection. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 171\u2013187. Springer, Heidelberg (2009)"},{"key":"21_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-03331-5","volume-title":"\u00dcbersetzerbau: Analyse und Transformation","author":"H. Seidl","year":"2010","unstructured":"Seidl, H., Wilhelm, R., Hack, S.: \u00dcbersetzerbau: Analyse und Transformation. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:34Z","timestamp":1619785054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}