12 Pages
English

The Verification Grand Challenge and Abstract Interpretation

-

Gain access to the library to view online
Learn more

Description

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


Subjects

Informations

Published by
Reads 14
Language English
TheVerificationGrandChallengeandAbstractInterpretationPatrickCousot1E´colenormalesupe´rieure45rued’Ulm75230Pariscedex05FrancePatrick.Cousot@ens.fr1IntroductionAbstractInterpretationisatheoryofapproximationofmathematicalstructures,inparticularthoseinvolvedinthesemanticmodelsofcomputersystems[4,10,11].Abstractinterpretationcanbeappliedtothesystematicconstructionofmethodsandeffectivealgorithmstoapproximateundecidableorverycomplexproblemsincomputerscience.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,whichprovidesdirectionsforapplicationofabstractinterpretationtotheVerificationGrandChallenge[22,23].2TheStaticAnalyzerASTRE´E2.1ProgramsanalyzedbyASTRE´EAstre´e[1,2,3,17,18,25]isastaticprogramanalyzeraimingatprovingtheab-senceofRunTimeErrors(RTE)inprogramswrittenintheCprogramminglanguage1.Astre´eanalyzesstructuredCprograms,withoutsideeffectsinexpressions,dynamicmemoryallocationandrecursion.AllotherfeaturesofCarehandledincludingarrays,structures,uniontypes,pointers,pointerarithmetics,etc[31].1Cprogramsareanalyzedaftermacro-expansion.