The Verification Grand Challenge and Abstract Interpretation

pages

English

Documents

Écrit par
Patrick Cousot1

Publié par
profil-zyak-2012

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

profil-zyak-2012

Nombre de lectures

Langue

English

Niveau: Supérieur, Doctorat, Bac+8
The Verification Grand Challenge and Abstract Interpretation Patrick Cousot1 Ecole normale superieure 45 rue d'Ulm 75230 Paris cedex 05 France n ru f. oi C st eokr .@t sP ca 1 Introduction Abstract Interpretation is a theory of approximation of mathematical structures, in particular those involved in the semantic models of computer systems [4,10,11]. Abstract interpretation can be applied to the systematic construction of methods and effective algorithms to approximate undecidable or very complex problems in computer science. The scope of application is rather large e.g. from type inference [5], model-checking [13], program transformation [14], watermarking [15] to context-free grammar parser generation [16]. In particular, abstract interpretation-based static analysis, which automat- ically infers dynamic properties of computer systems, has been very successful these last years to automatically verify complex properties of real-time, safety critical, embedded systems. For example, Astree [1,2,3,17,18,25] can analyze mechanically and verify formally the absence of runtime errors in industrial safety-critical embedded synchronous control/command codes of several hundred thousand to one million of lines C. We summarize the main reasons for the technical success of Astree, which provides directions for application of abstract interpretation to the Verification Grand Challenge [22,23].

can rely

abstract interpretation

attribute-independent abstract

based static

programs

verification only

static analyzers

since execution

astree

Voir

Publié par

profil-zyak-2012

Nombre de lectures

Langue

English

TheVeriﬁcationGrandChallengeandAbstractInterpretationPatrickCousot1E´colenormalesupe´rieure45rued’Ulm75230Pariscedex05FrancePatrick.Cousot@ens.fr1IntroductionAbstractInterpretationisatheoryofapproximationofmathematicalstructures,inparticularthoseinvolvedinthesemanticmodelsofcomputersystems[4,10,11].Abstractinterpretationcanbeappliedtothesystematicconstructionofmethodsandeﬀectivealgorithmstoapproximateundecidableorverycomplexproblemsincomputerscience.Thescopeofapplicationisratherlargee.g.fromtypeinference[5],model-checking[13],programtransformation[14],watermarking[15]tocontext-freegrammarparsergeneration[16].Inparticular,abstractinterpretation-basedstaticanalysis,whichautomat-icallyinfersdynamicpropertiesofcomputersystems,hasbeenverysuccessfultheselastyearstoautomaticallyverifycomplexpropertiesofreal-time,safetycritical,embeddedsystems.Forexample,Astre´e[1,2,3,17,18,25]cananalyzemechanicallyandverifyformallytheabsenceofruntimeerrorsinindustrialsafety-criticalembeddedsynchronouscontrol/commandcodesofseveralhundredthousandtoonemillionoflinesC.WesummarizethemainreasonsforthetechnicalsuccessofAstre´e,whichprovidesdirectionsforapplicationofabstractinterpretationtotheVeriﬁcationGrandChallenge[22,23].2TheStaticAnalyzerASTRE´E2.1ProgramsanalyzedbyASTRE´EAstre´e[1,2,3,17,18,25]isastaticprogramanalyzeraimingatprovingtheab-senceofRunTimeErrors(RTE)inprogramswrittenintheCprogramminglanguage1.Astre´eanalyzesstructuredCprograms,withoutsideeﬀectsinexpressions,dynamicmemoryallocationandrecursion.AllotherfeaturesofCarehandledincludingarrays,structures,uniontypes,pointers,pointerarithmetics,etc[31].1Cprogramsareanalyzedaftermacro-expansion.

Voir