{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T04:05:34Z","timestamp":1791345934427,"version":"4.3.1"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,11,11]],"date-time":"2009-11-11T00:00:00Z","timestamp":1257897600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s10703-009-0089-6","type":"journal-article","created":{"date-parts":[[2009,11,10]],"date-time":"2009-11-10T16:23:06Z","timestamp":1257870186000},"page":"229-264","source":"Crossref","is-referenced-by-count":92,"title":["Why does Astr\u00e9e scale up?"],"prefix":"10.1007","volume":"35","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radhia","family":"Cousot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00e9r\u00f4me","family":"Feret","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurent","family":"Mauborgne","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2009,11,11]]},"reference":[{"key":"89_CR1","series-title":"LNCS","first-page":"3","volume-title":"Proc 12th int symp SAS \u201905","author":"R Bagnara","year":"2005","unstructured":"Bagnara R, Hill PM, Mazzi E, Zaffanella E (2005) Widening operators for weakly-relational numeric abstractions. In: Hankin C, Siveroni I (eds) Proc 12th int symp SAS \u201905, London, 7\u20139 Sep 2005. LNCS, vol 3672. Springer, Berlin, pp 3\u201318"},{"key":"89_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The essence of computation: complexity, analysis, transformation. Essays dedicated to Neil D Jones","author":"B Blanchet","year":"2002","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen T, Schmidt DA, Sudborough IH (eds) The essence of computation: complexity, analysis, transformation. Essays dedicated to Neil D Jones. LNCS, vol 2566. Springer, Berlin, pp 85\u2013108"},{"key":"89_CR3","first-page":"196","volume-title":"Proc ACM SIGPLAN \u20192003 conf PLDI","author":"B Blanchet","year":"2003","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Proc ACM SIGPLAN \u20192003 conf PLDI, San Diego, 7\u201314 June 2003. ACM, New York, pp 196\u2013207"},{"key":"89_CR4","series-title":"LNCS","first-page":"128","volume-title":"Proc FMPA","author":"F Bourdoncle","year":"1993","unstructured":"Bourdoncle F (1993) Efficient chaotic iteration strategies with widenings. In: Bj\u00f8rner D, Broy M, Pottosin IV (eds) Proc FMPA, Akademgorodok, Novosibirsk, 28 June\u20132 July 1993. LNCS, vol 735. Springer, Berlin, pp 128\u2013141"},{"key":"89_CR5","doi-asserted-by":"crossref","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C 35(8)","DOI":"10.1109\/TC.1986.1676819"},{"key":"89_CR6","series-title":"Proc IFIP congress","first-page":"308","volume-title":"Information Processing 74","author":"RM Burstall","year":"1974","unstructured":"Burstall RM (1974) Program proving as hand simulation with a little induction. In: Rosenfeld JL (ed) Information Processing 74, Stockholm, Aug 5\u201310 1974. Proc IFIP congress, vol 74. North-Holland, Amsterdam, pp 308\u2013312"},{"key":"89_CR7","series-title":"LNCS","first-page":"154","volume-title":"Proc 12th int conf CAV \u201900","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP (eds) Proc 12th int conf CAV \u201900, Chicago, 15\u201319 Jul 2000. LNCS, vol 1855. Springer, Berlin, pp 154\u2013169"},{"key":"89_CR8","series-title":"LNCS","first-page":"168","volume-title":"Proc 10th int conf TACAS \u20192004","author":"EM Clarke","year":"2004","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Proc 10th int conf TACAS \u20192004, Barcelona, 29 Mar\u20132 Apr 2004. LNCS, vol 2988. Springer, Berlin, pp 168\u2013176"},{"key":"89_CR9","first-page":"195","volume-title":"23rd POPL","author":"C Colby","year":"1996","unstructured":"Colby C, Lee P (1996) Trace-based program analysis. In: 23rd POPL, St Petersburg Beach, 1996. ACM, New York, pp 195\u2013207"},{"key":"89_CR10","unstructured":"Cousot P (1978) M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes. Th\u00e8se d\u2019\u00c9tat \u00e8s sciences math\u00e9matiques, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble, Grenoble, 21 Mar 1978"},{"key":"89_CR11","first-page":"303","volume-title":"Program flow analysis: theory and applications","author":"P Cousot","year":"1981","unstructured":"Cousot P (1981) Semantic foundations of program analysis. In: Muchnick SS, Jones ND (eds) Program flow analysis: theory and applications. Prentice Hall, New York, pp 303\u2013342. Chap\u00a010"},{"key":"89_CR12","series-title":"NATO science series, series\u00a0F: computer and systems sciences","first-page":"421","volume-title":"Calculational system design","author":"P Cousot","year":"1999","unstructured":"Cousot P (1999) The calculational design of a generic abstract interpreter. In: Broy M, Steinbr\u00fcggen R (eds) Calculational system design. NATO science series, series\u00a0F: computer and systems sciences, vol 173. IOS Press, Amsterdam, pp 421\u2013505"},{"key":"89_CR13","series-title":"LNAI","first-page":"1","volume-title":"Proc 4th int symp SARA \u20192000","author":"P Cousot","year":"2000","unstructured":"Cousot P (2000) Partial completeness of abstract fixpoint checking. In: Choueiry BY, Walsh T (eds) Proc 4th int symp SARA \u20192000, Horseshoe Bay, 26\u201329 Jul 2000. LNAI, vol 1864. Springer, Berlin, pp 1\u201325"},{"key":"89_CR14","first-page":"106","volume-title":"Proc 2nd int symp on programming","author":"P Cousot","year":"1976","unstructured":"Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: Proc 2nd int symp on programming. Dunod, Paris, pp 106\u2013130"},{"key":"89_CR15","first-page":"238","volume-title":"4th POPL","author":"P Cousot","year":"1977","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a\u00a0unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th POPL, Los Angeles, 1977. ACM, New York, pp\u00a0238\u2013252"},{"key":"89_CR16","first-page":"269","volume-title":"6th POPL","author":"P Cousot","year":"1979","unstructured":"Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: 6th POPL, San Antonio, 1979. ACM, New York, pp 269\u2013282"},{"key":"89_CR17","first-page":"43","volume-title":"Tools & notions for program construction","author":"P Cousot","year":"1982","unstructured":"Cousot P, Cousot R (1982) Induction principles for proving invariance properties of programs. In: N\u00e9el D (ed) Tools & notions for program construction. Cambridge University Press, Cambridge, pp 43\u2013119"},{"key":"89_CR18","series-title":"LNCS","first-page":"269","volume-title":"Proc 4th int symp on PLILP \u201992","author":"P Cousot","year":"1992","unstructured":"Cousot P, Cousot R (1992) Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe M, Wirsing M (eds) Proc 4th int symp on PLILP \u201992, Leuven, 26\u201328 Aug 1992. LNCS, vol 631. Springer, Berlin, pp 269\u2013295"},{"key":"89_CR19","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(93)90248-R","volume":"120","author":"P Cousot","year":"1993","unstructured":"Cousot P, Cousot R (1993) \u201c\u00c0 la Burstall\u201d intermittent assertions induction principles for proving inevitability properties of programs. Theor Comput Sci 120:123\u2013155","journal-title":"Theor Comput Sci"},{"key":"89_CR20","series-title":"LNCS","first-page":"159","volume-title":"Proc 11th int conf CC \u20192002","author":"P Cousot","year":"2002","unstructured":"Cousot P, Cousot R (2002) Modular static program analysis. In: Horspool RN (ed) Proc 11th int conf CC \u20192002, Grenoble, 6\u201314 Apr 2002. LNCS, vol 2304. Springer, Berlin, pp 159\u2013178"},{"key":"89_CR21","first-page":"84","volume-title":"5th POPL","author":"P Cousot","year":"1978","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: 5th POPL, Tucson, 1978. ACM, New York, pp 84\u201397"},{"key":"89_CR22","series-title":"LNCS","first-page":"21","volume-title":"Proc 14th ESOP \u20192005","author":"P Cousot","year":"2005","unstructured":"Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2005) The Astr\u00e9e analyser. In: Sagiv M (ed) Proc 14th ESOP \u20192005, Edinburg, 2\u201310 Apr 2005. LNCS, vol 3444. Springer, Berlin, pp 21\u201330"},{"key":"89_CR23","first-page":"3","volume-title":"Proc 1st TASE \u201907","author":"P Cousot","year":"2007","unstructured":"Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2007) Varieties of static analyzers: A\u00a0comparison with Astr\u00e9e. In: Hinchey M, Jifeng H, Sanders J (eds) Proc 1st TASE \u201907, Shanghai, 6\u20138 June 2007. IEEE Comput Soc, Los Alamitos, pp 3\u201317"},{"key":"89_CR24","series-title":"LNCS","first-page":"333","volume-title":"Proc 14th int symp SAS \u201907","author":"P Cousot","year":"2007","unstructured":"Cousot P, Ganty P, Raskin J-F (2007) Fixpoint-guided abstraction refinements. In: Fil\u00e9 G, Riis-Nielson H (eds) Proc 14th int symp SAS \u201907, Kongens Lyngby, 22\u201324 Aug 2007. LNCS, vol 4634. Springer, Berlin, pp 333\u2013348"},{"key":"89_CR25","series-title":"LNCS","first-page":"272","volume-title":"11th ASIAN 06","author":"P Cousot","year":"2008","unstructured":"Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2008) Combination of abstractions in the Astr\u00e9e static analyzer. In: Okada M, Satoh I (eds) 11th ASIAN 06, Tokyo, 6\u20138 Dec 2006. LNCS, vol 4435. Springer, Berlin, pp 272\u2013300"},{"key":"89_CR26","series-title":"LNCS","first-page":"437","volume-title":"Proc 14th int symp SAS \u201907","author":"D Delmas","year":"2007","unstructured":"Delmas D, Souyris J (2007) Astr\u00e9e: from research to industry. In: Fil\u00e9 G, Riis-Nielson H (eds) Proc 14th int symp SAS \u201907, Kongens Lyngby, 22\u201324 Aug 2007. LNCS, vol 4634. Springer, Berlin, pp 437\u2013451"},{"issue":"7","key":"89_CR27","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva V, Kroening D, Weissenbacher G (2008) A survey of automated techniques for formal software verification. IEEE Trans Comput-Aided Des Integr Circuits 27(7):1165\u20131178","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits"},{"key":"89_CR28","series-title":"LNCS","first-page":"33","volume-title":"Proc 30th ESOP \u20192004","author":"J Feret","year":"2004","unstructured":"Feret J (2004) Static analysis of digital filters. In: Schmidt D (ed) Proc 30th ESOP \u20192004, Barcelona, Mar 27\u2013Apr 4, 2004. LNCS, vol 2986. Springer, Berlin, pp 33\u201348"},{"key":"89_CR29","series-title":"LNCS","first-page":"42","volume-title":"Proc 6th int conf VMCAI 2005","author":"J Feret","year":"2005","unstructured":"Feret J (2005) The arithmetic-geometric progression abstract domain. In: Cousot R (ed) Proc 6th int conf VMCAI 2005, Paris, 17\u201319 Jan 2005. LNCS, vol 3385. Springer, Berlin, pp 42\u201358"},{"key":"89_CR30","unstructured":"Feret J (2005) Numerical abstract domains for digital filters. In: 1st int work on numerical & symbolic abstract domains, NSAD \u201905, Maison Des Polytechniciens, Paris, 21 Jan 2005"},{"key":"89_CR31","first-page":"655","volume-title":"Proc int symp ILPS \u20191994","author":"G Fil\u00e9","year":"1994","unstructured":"Fil\u00e9 G, Ranzato F (1994) Improving abstract interpretations by systematic lifting to the powerset. In: Bruynooghe M (ed) Proc int symp ILPS \u20191994, Ithaca, 13\u201317 Nov 1994. MIT Press, Cambridge, pp\u00a0655\u2013669"},{"key":"89_CR32","first-page":"19","volume-title":"Proc symposium in applied mathematics","author":"RW Floyd","year":"1967","unstructured":"Floyd RW (1967) Assigning meaning to programs. In: Schwartz JT (ed) Proc symposium in applied mathematics, vol 19. AMS, Providence, pp 19\u201332"},{"issue":"1\u20133","key":"89_CR33","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0167-6423(97)00034-8","volume":"32","author":"R Giacobazzi","year":"1998","unstructured":"Giacobazzi R, Ranzato F (1998) Optimal domains for disjunctive abstract interpretation. Sci Comput Program 32(1\u20133):177\u2013210","journal-title":"Sci Comput Program"},{"issue":"2","key":"89_CR34","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R Giacobazzi","year":"2000","unstructured":"Giacobazzi R, Ranzato F, Scozzari F (2000) Making abstract interpretations complete. J ACM 47(2):361\u2013416","journal-title":"J ACM"},{"key":"89_CR35","series-title":"LNCS","first-page":"234","volume-title":"Proc 8th int symp SAS \u201901","author":"\u00c9 Goubault","year":"2001","unstructured":"Goubault \u00c9 (2001) Static analyses of floating-point operations. In: Cousot P (ed) Proc 8th int symp SAS \u201901, Paris, Jul 2001. LNCS, vol 2126. Springer, Berlin, pp 234\u2013259"},{"key":"89_CR36","series-title":"LNCS","first-page":"209","volume-title":"Proc 11th ESOP \u20192002","author":"\u00c9 Goubault","year":"2002","unstructured":"Goubault \u00c9, Martel M, Putot S (2002) Asserting the precision of floating-point computations: a simple abstract interpreter. In: Le M\u00e9tayer D (ed) Proc 11th ESOP \u20192002, Grenoble, 8\u201312 Apr 2002. LNCS, vol\u00a02305. Springer, Berlin, pp 209\u2013212"},{"key":"89_CR37","series-title":"LNCS","first-page":"196","volume-title":"Proc 8th int conf CAV \u201997","author":"S Graf","year":"1996","unstructured":"Graf S, Sa\u00efdi H (1996) Verifying invariants using theorem proving. In: Alur R, Henzinger TA (eds) Proc 8th int conf CAV \u201997, New Brunswick, Jul 31\u2013Aug 3, 1996. LNCS, vol 1102. Springer, Berlin, pp\u00a0196\u2013207"},{"issue":"3 & 4","key":"89_CR38","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1080\/00207168908803778","volume":"30","author":"P Granger","year":"1989","unstructured":"Granger P (1989) Static analysis of arithmetical congruences. Int J Comput Math 30(3 & 4):165\u2013190","journal-title":"Int J Comput Math"},{"key":"89_CR39","unstructured":"Granger P (1991) Improving the results of static analyses of programs by local decreasing iterations. Res rep. LIX\/RR\/91\/08, Laboratoire d\u2019Informatique, \u00c9cole polytechnique, Palaiseau, Dec 1991"},{"key":"89_CR40","series-title":"LNCS","first-page":"443","volume-title":"Proc 14th int conf TACAS \u20192000","author":"BS Gulavani","year":"2008","unstructured":"Gulavani BS, Chakraborty S, Nori AV, Rajamani SK (2008) Automatically refining abstract interpretations. In: Ramakrishnan CR, Rehof J (eds) Proc 14th int conf TACAS \u20192000, Budapest, 29 Mar\u20136 Apr 2008. LNCS, vol 4963. Springer, Berlin, pp 443\u2013458"},{"key":"89_CR41","series-title":"LNCS","first-page":"200","volume-title":"Proc 5th int symp SAS \u201998","author":"M Handjieva","year":"1998","unstructured":"Handjieva M, Tzolovski S (1998) Refining static analyses by trace-based partitioning using control flow. In: Levi G (ed) Proc 5th int symp SAS \u201998, Pisa, 14\u201316 Sep 1998. LNCS, vol 1503. Springer, Berlin, pp\u00a0200\u2013214"},{"key":"89_CR42","volume-title":"Flow analysis of computer programs","author":"MS Hecht","year":"1977","unstructured":"Hecht MS (1977) Flow analysis of computer programs. North-Holland\/Elsevier, Amsterdam"},{"issue":"10","key":"89_CR43","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580","journal-title":"Commun ACM"},{"key":"89_CR44","unstructured":"Jeannet B, Min\u00e9 A (2007) The Apron numerical abstract domain library. http:\/\/apron.cri.ensmp.fr\/library\/"},{"key":"89_CR45","unstructured":"Lacan P, Monfort JN, Ribal LVQ, Deutsch A, Gonthier G (1998) The software reliability verification process: The Ariane 5 example. In Proceedings DASIA 98\u2014DAta Systems In Aerospace, Athens. ESA Publications, SP-422, 25\u201328 May 1998"},{"key":"89_CR46","unstructured":"Leroy X, Doligez D, Garrigue J, R\u00e9my D, Vouillon J (2007) The Objective Caml system, documentation and user\u2019s manual (release 3.10). Technical report, INRIA, Rocquencourt, France, 19 May 2007. http:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/"},{"key":"89_CR47","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/978-1-4020-8157-6_30","volume-title":"Building the information society","author":"L Mauborgne","year":"2004","unstructured":"Mauborgne L (2004) Astr\u00e9e: Verification of absence of run-time error. In: Jacquart P (ed) Building the information society. Kluwer Academic, Norwell, pp 385\u2013392. Chap\u00a04"},{"key":"89_CR48","series-title":"LNCS","first-page":"5","volume-title":"Proc 14th ESOP \u20192005","author":"L Mauborgne","year":"2005","unstructured":"Mauborgne L, Rival X (2005) Trace partitioning in abstract interpretation based static analyzer. In: Sagiv M (ed) Proc 14th ESOP \u20192005, Edinburg, Apr 2\u201310, 2005. LNCS, vol 3444. Springer, Berlin, pp 5\u201320"},{"key":"89_CR49","series-title":"LNCS","first-page":"3","volume-title":"Proc 30th ESOP \u20192004","author":"A Min\u00e9","year":"2004","unstructured":"Min\u00e9 A (2004) Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt D (ed) Proc 30th ESOP \u20192004, Barcelona, Mar 27\u2013Apr 4, 2004. LNCS, vol 2986. Springer, Berlin, pp 3\u201317"},{"key":"89_CR50","unstructured":"Min\u00e9 A (2004) Weakly relational numerical abstract domains. Th\u00e8se de doctorat en informatique, \u00c9cole polytechnique, Palaiseau, 6 Dec 2004"},{"key":"89_CR51","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/1134650.1134659","volume-title":"Proc LCTES \u20192006","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9 A (2006) Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Proc LCTES \u20192006. ACM, New York, pp 54\u201363"},{"key":"89_CR52","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9 A (2006) The octagon abstract domain. High-Order Symb Comput 19:31\u2013100","journal-title":"High-Order Symb Comput"},{"key":"89_CR53","series-title":"LNCS","first-page":"348","volume-title":"Proc 7th int conf VMCAI 2006","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9 A (2006) Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson EA, Namjoshi KS (eds) Proc 7th int conf VMCAI 2006, Charleston, 8\u201310 Jan 2006. LNCS, vol 3855. Springer, Berlin, pp 348\u2013363"},{"key":"89_CR54","series-title":"LNCS","first-page":"86","volume-title":"Proc 3rd APLAS \u20192005","author":"D Monniaux","year":"2005","unstructured":"Monniaux D (2005) The parallel implementation of the Astr\u00e9e static analyzer. In: Proc 3rd APLAS \u20192005, Tsukuba, 3\u20135 Nov 2005. LNCS, vol 3780. Springer, Berlin, pp 86\u201396"},{"key":"89_CR55","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/BF01966091","volume":"6","author":"P Naur","year":"1966","unstructured":"Naur P (1966) Proofs of algorithms by general snapshots. BIT 6:310\u2013316","journal-title":"BIT"},{"key":"89_CR56","unstructured":"Pioli A, Hind M (1999) Combining interprocedural pointer analysis and conditional constant propagation. Technical Report 99-103, IBM"},{"key":"89_CR57","unstructured":"Randimbivololona F, Souyris J, Deutsch A (2000) Improving avionics software verification cost-effectiveness: Abstract interpretation based technology contribution. In: Proceedings DASIA 2000\u2014DAta Systems In Aerospace, Montreal. ESA Publications, 22\u201326 May 2000"},{"key":"89_CR58","doi-asserted-by":"crossref","unstructured":"Rival X, Mauborgne L (2007) The trace partitioning abstract domain. TOPLAS 29(5)","DOI":"10.1145\/1275497.1275501"},{"key":"89_CR59","first-page":"105","volume-title":"26th POPL","author":"M Sagiv","year":"1999","unstructured":"Sagiv M, Reps T, Wilhelm R (1999) Parametric shape analysis via 3-valued logic. In: 26th POPL, San Antonio, 1999. ACM, New York, pp 105\u2013118"},{"key":"89_CR60","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/978-1-4020-8157-6_31","volume-title":"Building the information society","author":"J Souyris","year":"2004","unstructured":"Souyris J (2004) Industrial experience of abstract interpretation-based static analyzers. In: Jacquart P (ed) Building the information society. Kluwer Academic, Norwell, pp 393\u2013400. Chap\u00a04"},{"key":"89_CR61","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/978-3-540-75101-4_45","volume-title":"Proc int conf on computer safety, reliability, and security (Safecomp 2007)","author":"J Souyris","year":"2007","unstructured":"Souyris J, Delmas D (2007) Experimental assessment of Astr\u00e9e on safety-critical avionics software. In: Saglietti F, Oster N (eds) Proc int conf on computer safety, reliability, and security (Safecomp 2007), Nuremberg, 18\u201321 Sep 2007. LNCS, vol 4680. Springer, Berlin, pp 479\u2013490"},{"issue":"1","key":"89_CR62","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1016\/j.tcs.2005.07.035","volume":"345","author":"Z Su","year":"2005","unstructured":"Su Z, Wagner D (2005) A class of polynomially solvable range constraints for interval analysis without widenings. Theor Comput Sci 345(1):122\u2013138","journal-title":"Theor Comput Sci"},{"key":"89_CR63","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-1-4020-8157-6_18","volume-title":"Building the information society","author":"P Traverse","year":"2004","unstructured":"Traverse P, Lacaze I, Souyris J (2004) Airbus fly-by-wire\u2014a\u00a0total approach to dependability. In: Jacquart P (ed) Building the information society. Kluwer Academic, Norwell, pp 191\u2013212, Chap\u00a03"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0089-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0089-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0089-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:51Z","timestamp":1559253951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0089-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11,11]]},"references-count":63,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["89"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0089-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,11,11]]}}}