Shape analysis through predicate abstraction and model check(14)

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

paringtheGaloisconnectionandwiden-ing/narrowingapproachestoabstractinterpretation.InM.BruynoogheandM.Wirsing,editors,ProgrammingLanguageImplementationandLogicProgram-ming,volume631ofLNCS,pages269–295,1992.

9.S.DasandD.Dill.Successiveapproximationofabstracttransitionrelations.InLICS,2001.

10.S.Das,D.Dill,andS.Park.Experiencewithpredicateabstraction.InCAV,

volume1633ofLNCS,1999.

11.M.DavisandH.Putnam.Acomputingprocedureforquanti cationtheory.J.

putingMachinery,7:201–215,1960.

12.E.W.Dijkstra.Guardedcommands,nondeterminacy,andformalderivationof

programs.C.ACM,18,1975.

13.C.FlanaganandS.Qadeer.Predicateabstractionforsoftwareveri cation.In

POPL,2002.

14.S.GrafandH.Sa¨ di.ConstructionofabstractstategraphswithPVS.InCAV,

volume1254ofLNCS,1997.

15.D.Gries.TheScienceOfProgramming.Springer-Verlag,1981.

16.R.H.Hardin,Z.Har’el,andR.P.Kurshan.COSPAN.InCAV,volume1102of

LNCS,1996.

17.T.A.Henzinger,R.Jhala,R.Majumdar,zyabstraction.InPOPL,

2002.

18.G.Holzmann.TheSPINmodelchecker.IEEETransactionsonSoftwareEngi-

neering,23(5),May1997.

19.J.L.Jensen,M.E.Jørgensen,N.Klarlund,andM.I.Schwartzbach.Automatic

veri cationofpointerprogramsusingmonadicsecond-orderlogic.InSIGPLANConferenceonProgrammingLanguageDesignandImplementation,pages226–236,1997.

20.M.Kaufmann,P.Manolios,puter-AidedReasoning:AnAp-

proach.KluwerAcademicPublishers,2000.

21.N.KlarlundandM.I.Schwartzbach.Graphsanddecidabletransductionsbased

onedgeconstraints(extendedabstract).InColloquiumonTreesinAlgebraandProgramming,pages187–201,1994.

khnech,S.Bensalem,S.Berezin,andS.Owre.Incrementalveri cationby

abstraction.InTACAS,volume2031ofLNCS,2001.

23.D.Lesens,N.Halbwachs,andP.Raymond.Automaticveri cationofparameter-

izednetworksofprocesses.TheoreticalComputerScience,256:113–144,2001.

LA:Asystemforimplementingstaticanalyses.In

SAS,volume1824ofLNCS,2000.

25.J.Morris.(1)Ageneralaxiomofassignment(2)Assignmentandlinkeddata

structures.InM.BroyandG.Schmidt,editors,TheoreticalFoundationsofPro-grammingMethodology,1981.

26.K.S.NamjoshiandR.P.Kurshan.Syntacticprogramtransformationsforauto-

maticabstraction.InCAV,volume1855ofLNCS,2000.

27.G.Nelson.Verifyingreachabilityinvariantsoflinkedstructures.InPOPL,1983.

28.N.RinetzkyandS.Sagiv.Interproceduralshapeanalysisforrecursiveprograms.

InComputationalComplexity,pages133–149,2001.

29.M.Sagiv,T.Reps,andR.Wilhelm.Parametricshapeanalysisvia3-valuedlogic.

TOPLAS,24(3):217–298,2002.

30.D.A.SchmidtandB.Ste en.Programanalysisasmodelcheckingofabstract

interpretations.InSAS,volume1503ofLNCS,1998.