Shape analysis through predicate abstraction and model check(13)

Abstract. We propose a new framework, based on predicate abstraction and model checking, for shape analysis of programs. Shape analysis is used to statically collect information — such as possible reachability and sharing — about program stores. Rather t

predicatesfromtheproperty,naturallyidentifyotherrelevantpredicates,includ-ingalloftheneededinstrumentationpredicates.Ontheotherhand,theTVLAtoolanalyzesthelistreversalexamplefullyautomatically,incontrasttoouruseofuser-suppliedapproximationhints.However,webelievethatitispossibletoautomatetheheuristicswehaveusedforidentifyingapproximations,sothatprogramssuchasthisarehandledfullyautomatically.

In[25,27],wpforreachabilityiscalculated,butnoothershapepredicatesareconsidered.Predicateabstraction,combinedwithmodelchecking,hasbeenusedinanalysesofsomeheapproperties:points-toanalysis[1],correctnessofconcur-rentgarbagecollectors[10,9],andloopinvariants[13].Thesepapers,however,donothandleshapeproperties.

Inconclusion,webelievethattheseparationofconcernsbetweenabstractionandstatespaceexplorationthatisproposedinthenewframeworkopensupsev-eralpossibilities.Theabstractionmethodservestodiscoverthepredicatesthatarerelevantforprovingagivenproperty.Thewpcalculationsperformabstrac-tionlocally,leavingtheglobalstatespaceexplorationtoamodelchecker.Onecanthustakeadvantageofhighlyoptimizedmodelcheckingimplementations,andthewidevarietyoflogicsandsystemmodelstowhichtheyapply.Ourinitialexperiencehas,wehope,demonstratedthepromiseofthismethod,whilerais-ingseveralinterestingquestionsfortheoreticalinvestigationsandexperimentalimprovements.

Ourongoinge ortsarefocusedonmechanizingtheheuristicsforapprox-imations.Astheveri cationproblemforshapepropertiesisundecidable,wecannothopeforafullyautomatedprocedurethatworksonallinstances.How-ever,therehavebeensuccessfulattempts[23]toautomatesimilarapproximationheuristicsusingrecognitionofpatterngrowthin(regular)expressions,basedontheframeworkofwidening[7,8].Also,wecanpotentiallybene tfromthede-signoftheoremprovingtools,suchasACL2[20],whichsuccessfullyrecognizeinductionpatternsinmanycases.

References

1.T.Ball,R.Majumdar,T.D.Millstein,andS.K.Rajamani.AutomaticpredicateabstractionofCprograms.InPLDI,2001.

2.T.Ball,A.Podelski,andS.Rajamani.Relativecompletenessofabstractionre- nementforsoftwaremodelchecking.InTACAS,volume2280ofLNCS,2002.

3.T.BallandS.Rajamani.TheSLAMtoolkit.InCAV,volume2102ofLNCS,2001.

4.M.Benedikt,T.Reps,andM.Sagiv.Adecidablelogicfordescribinglinkeddatastructures.InESOP,volume1576ofLNCS,pages2–19,1999.

5.R.Bornat.ProvingpointerprogramsinHoarelogic.InMathematicsofProgramConstruction,volume1837ofLNCS,pages102–126,2000.

6.E.M.Clarke,O.Grumberg,S.Jha,Y.Lu,andH.Veith.Counterexample-guidedabstractionre nement.InCAV,volume1855ofLNCS,2000.

7.P.CousotandR.Cousot.Abstractinterpretation:Auni edlatticemodelforstaticanalysisofprogramsbyconstructionorapproximationof xpoints.InPOPL,pages238–252,1977.