The Verification Grand Challenge and Abstract Interpretation

Patrick Cousot1

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

Sujets

• Error (disambiguation)
• Abstract interpretation
• Program
• Astrée

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 14
• Langue: English

Extrait

TheVerificationGrandChallenge andAbstractInterpretation PatrickCousot 1 E ´ colenormalesupe´rieure 45rued’Ulm 75230Pariscedex05 France [e-mail] 1Introduction AbstractInterpretationisatheoryofapproximationofmathematicalstructures, inparticularthoseinvolvedinthesemanticmodelsofcomputersystems[4,10,11]. Abstractinterpretationcanbeappliedtothesystematicconstructionofmethods andeffectivealgorithmstoapproximateundecidableorverycomplexproblems incomputerscience.Thescopeofapplicationisratherlargee.g.fromtype inference[5],model-checking[13],programtransformation[14],watermarking [15]tocontext-freegrammarparsergeneration[16]. Inparticular,abstractinterpretation-basedstaticanalysis,whichautomat- icallyinfersdynamicpropertiesofcomputersystems,hasbeenverysuccessful theselastyearstoautomaticallyverifycomplexpropertiesofreal-time,safety critical,embeddedsystems. Forexample, Astre ´ e [1,2,3,17,18,25]cananalyzemechanicallyandverify formallytheabsenceofruntimeerrorsinindustrialsafety-criticalembedded synchronouscontrol/commandcodesofseveralhundredthousandtoonemillion oflinesC. Wesummarizethemainreasonsforthetechnicalsuccessof Astre ´ e ,which providesdirectionsforapplicationofabstractinterpretationtotheVerification GrandChallenge[22,23]. 2TheStaticAnalyzerA STRE ´ E 2.1ProgramsanalyzedbyA STRE ´ E Astre ´ e [1,2,3,17,18,25]isastaticprogramanalyzeraimingatprovingtheab- senceofRunTimeErrors(RTE)inprogramswrittenintheCprogramming language 1 . Astre ´ e analyzesstructuredCprograms,withoutsideeffectsinexpressions, dynamicmemoryallocationandrecursion.AllotherfeaturesofCarehandled includingarrays,structures,uniontypes,pointers,pointerarithmetics,etc[31]. 1 Cprogramsareanalyzedaftermacro-expansion.