HTTP/2 200 date: Wed, 04 Feb 2026 11:33:41 GMT content-type: application/json content-length: 3037 access-control-expose-headers: Link access-control-allow-headers: X-Requested-With, Accept, Accept-Encoding, Accept-Charset, Accept-Language, Accept-Ranges, Cache-Control access-control-allow-origin: * vary: Accept-Encoding content-encoding: gzip server: Jetty(9.4.40.v20210413) x-rate-limit: 5 x-rate-limit-interval: 1s x-concurrency-limit: 1 x-api-pool: public permissions-policy: interest-cohort=() {"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T02:49:04Z","timestamp":1769741344756,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540003267","type":"print"},{"value":"9783540363774","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36377-7_5","type":"book-chapter","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T23:03:07Z","timestamp":1181170987000},"page":"85-108","source":"Crossref","is-referenced-by-count":106,"title":["Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Blanchet","sequence":"first","affiliation":[]},{"given":"Patrick","family":"Cousot","sequence":"additional","affiliation":[]},{"given":"Radhia","family":"Cousot","sequence":"additional","affiliation":[]},{"given":"J\u00e9r\u00f4me","family":"Feret","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Mauborgne","sequence":"additional","affiliation":[]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]},{"given":"David","family":"Monniaux","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proc. 2 nd Int. B Conf., B\u201998: Recent Advances in the Development and Use of the B Method","author":"J.-R. Abrial","year":"1998","unstructured":"J.-R. Abrial. On B. In D. Bert, editor, Proc. 2 nd Int. B Conf., B\u201998: Recent Advances in the Development and Use of the B Method, Montpellier, FR, LNCS 1393, pages 1\u20138. Springer-Verlag, 22-24 Apr. 1998."},{"key":"5_CR2","unstructured":"American National Standards Institute, Inc. IEEE standard for binary floatingpoint arithmetic. Technical Report 754-1985, ANSI\/IEEE, 1985. http:\/\/grouper.ieee.org\/groups\/754\/ ."},{"key":"5_CR3","unstructured":"P. R. Bevington and D. K. Robinson. Data Reduction and Error Analysis for the Physical Sciences. McGraw-Hill, 1992."},{"key":"5_CR4","unstructured":"P. Cousot. The Marktoberdorf\u201998 generic abstract interpreter. http:\/\/www.di.ens.fr\/~cousot\/Marktoberdorf98.shtml , Nov. 1998."},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","first-page":"138","volume-title":"Informatics-10 Years Back, 10 Years Ahead","author":"P. Cousot","year":"2000","unstructured":"P. Cousot. Abstract interpretation based formal methods and future challenges, invited paper. In R. Wilhelm, editor, Informatics-10 Years Back, 10 Years Ahead, volume 2000 of LNCS, pages 138\u2013156. Springer-Verlag, 2000. (minutes) Time"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot. Partial completeness of abstract fixpoint checking, invited paper. In B.Y. Choueiry and T. Walsh, editors, Proc. 4 th Int. Symp. SARA\u20192000, Horseshoe Bay, TX, US, LNAI 1864, pages 1\u201325. Springer-Verlag, 26-29 Jul. 2000.","DOI":"10.1007\/3-540-44914-0_1"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. 2 nd Int. Symp. on Programming, pages 106\u2013130. Dunod, 1976.","DOI":"10.1145\/390019.808314"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4 th POPL, pages 238\u2013252, Los Angeles, CA, 1977. ACM Press.","DOI":"10.1145\/512950.512973"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6 th POPL, pages 269\u2013282, San Antonio, TX, 1979. ACM Press.","DOI":"10.1145\/567752.567778"},{"issue":"1","key":"5_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D. Goldberg","year":"1991","unstructured":"D. Goldberg. What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv., 23(1):5\u201348, Mar. 1991.","journal-title":"ACM Comput. Surv"},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-49727-7_12","volume-title":"Proc. 5 th Int. Symp. SAS\u2019 98","author":"M. Handjieva","year":"1998","unstructured":"M. Handjieva and S. Tzolovski. Refining static analyses by trace-based partitioning using control flow. In G. Levi, editor, Proc. 5 th Int. Symp. SAS\u2019 98, Pisa, IT, 14-16 Sep. 1998, LNCS 1503, pages 200\u2013214. Springer-Verlag, 1998."},{"key":"5_CR12","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proc. 14 th Int. Conf. CAV\u20192002","author":"G.J. Holzmann","year":"2002","unstructured":"G.J. Holzmann. Software analysis and model checking. In E. Brinksma and K.G. Larsen, editors, Proc. 14 th Int. Conf. CAV\u20192002, Copenhagen, DK, LNCS 2404, pages 1\u201316. Springer-Verlag, 27-31 Jul. 2002."},{"key":"5_CR13","unstructured":"N. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Int. Series in Computer Science. Prentice-Hall, June 1993."},{"key":"5_CR14","unstructured":"JTC 1\/SC 22. Programming languages-C. Technical report, ISO\/IEC 9899:1999, 16 Dec. 1999."},{"key":"5_CR15","unstructured":"X. Leroy, D. Doligez, J. Garrigue, D. R\u00e9my, and J. Vouillon. The Objective Caml system, documentation and user\u2019s manual (release 3.04). Technical report, INRIA, Rocquencourt, FR, 10 Dec. 2001. http:\/\/caml.inria.fr\/ocaml\/ ."},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Proc. 2 nd Symp. PADO\u20192001","author":"A. Min\u00e9","year":"2001","unstructured":"A. Min\u00e9. A new numerical abstract domain based on difference-bound matrices. In 0. Danvy and A. Filinski, editors, Proc. 2 nd Symp. PADO\u20192001, \u00c5rhus, DK, 21-23 May 2001, LNCS 2053, pages 155\u2013172. Springer-Verlag, 2001. http:\/\/www.di.ens.fr\/~mine\/publi\/article-mine-padoII.pdf ."},{"key":"5_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-48257-1_24","volume-title":"PROC Applied Formal Methods-FM-Trends\u201998, International Workshop on Current Trends in Applied Formal Method","author":"S. Owre","year":"1999","unstructured":"S. Owre, N. Shankar, and D.W.J. Stringer-Calvert. PVS: An experience report. In D. Hutter, W. Stephan, P. Traverso, and M. Ullmann, editors, PROC Applied Formal Methods-FM-Trends\u201998, International Workshop on Current Trends in Applied Formal Method, Boppard, DE, LNCS 1641, pages 338\u2013345. Springer-Verlag, 7-9 Oct. 1999."}],"container-title":["Lecture Notes in Computer Science","The Essence of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36377-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T07:15:31Z","timestamp":1683875731000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36377-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540003267","9783540363774"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-36377-7_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}