Abstraction refinement via inductive learning

AlexeyLoginov1,ThomasReps1,andMoolySagiv2

1

Comp.Sci.Dept.,UniversityofWisconsin;{alexey,reps}@cs.wisc.edu2

SchoolofComp.Sci.,Tel-AvivUniversity;msagiv@post.tau.ac.il

Abstract.Thispaperconcernshowtoautomaticallycreateabstractionsforprogramanal-ysis.Weshowthatinductivelearning,thegoalofwhichistoidentifygeneralrulesfromasetofobservedinstances,providesnewleverageontheproblem.Anadvantageofanap-proachbasedoninductivelearningisthatitdoesnotrequiretheuseofatheoremprover.

1Introduction

Wepresentanapproachtoautomaticallycreatingabstractionsforuseinprogramanal-ysis.Asinsomepreviouswork[12,4,13,18,5,2,8],theapproachinvolvesthesucces-siverefinementoftheabstractioninuse.Unlikepreviouswork,theworkpresentedinthispaperisaimedatprogramsthatmanipulatepointersandheap-allocateddatastruc-tures.However,whilewedemonstrateourapproachonshape-analysisproblems,theapproachisapplicableinanyprogram-analysissettingthatusesfirst-orderlogic.

Thepaperpresentsanabstraction-refinementmethodforuseinstaticanalysesbasedon3-valuedlogic[21],wherethesemanticsofstatementsandthequeryofinterestareexpressedusinglogicalformulas.Inthissetting,amemoryconfigurationismodeledbyalogicalstructure;anindividualofthestructure’suniverseeithermodelsasin-glememoryelementor,inthecaseofasummaryindividual,itmodelsacollectionofmemoryelements.Summaryindividualsareusedtoensurethatabstractdescriptorshaveanaprioriboundedsize,whichguaranteesthatafixed-pointisalwaysreached.However,theconstraintofworkingwithlimited-sizedescriptorsimpliesalossofin-formationaboutthestore.Intuitively,certainpropertiesofconcreteindividualsarelostduetoabstraction,whichgroupstogethermultipleindividualsintosummaryindividu-als:apropertycanbetrueforsomeconcreteindividualsofthegroup,butfalseforotherindividuals.TheTVLAsystemisatoolforcreatingsuchanalyses[1].

Withthemethodproposedinthispaper,refinementisperformedbyintroducingnewinstrumentationrelations(definedvialogicalformulasovercorerelations,whichcap-turethebasicpropertiesofmemoryconfigurations).Instrumentationrelationsrecordauxiliaryinformationinalogicalstructure,thusprovidingamechanismtofine-tuneanabstraction:aninstrumentationrelationcapturesapropertythatanindividualmemorycellmayormaynotpossess.Ingeneral,theintroductionofadditionalinstrumentationrelationsrefinesanabstractionintoonethatispreparedtotrackfinerdistinctionsamongstores.Thechoiceofinstrumentationrelationsiscrucialtotheprecision,aswellasthecost,oftheanalysis.Untilnow,TVLAusershavebeenfacedwiththetaskofidenti-fyinganinstrumentation-relationsetthatgivesthemadefiniteanswertothequery,butdoesnotmakethecostprohibitive.ThiswasarguablythekeyremainingchallengeintheTVLAuser-model.Thecontributionsofthisworkcanbesummarizedasfollows:–Itestablishesanewconnectionbetweenprogramanalysisandmachinelearningbyshowingthatinductivelogicprogramming(ILP)[19,17,14]isrelevanttotheprob-lemofcreatingabstractions.WeuseILPforlearningnewinstrumentationrelationsthatpreserveinformationthatwouldotherwisebelostduetoabstraction.

–ThemethodhasbeenimplementedasanextensionofTVLA.Inthissystem,alloftheuser-levelobligationsforwhichTVLAhasbeencriticizedinthepasthavebeenaddressed.Theinputrequiredtospecifyaprogramanalysisconsistsof:(i)atransitionsystem,(ii)aquery(aformulathatidentifiesacceptableoutputs),and(iii)acharacterizationoftheprogram’svalidinputs.

–Wepresentexperimentalevidenceofthevalueoftheapproach.Wetestedthemethodonsortedness,stability,andantistabilityqueriesforasetofprogramsthatperformdestructivelistmanipulation,aswellasonpartial-correctnessqueriesfortwobinary-search-treeprograms.Themethodsucceedsinallcasestested.

Inductivelearningconcernsidentifyinggeneralrulesfromasetofobservedinstances—inourcase,fromrelationshipsobservedinalogicalstructure.Anadvantageofanap-proachbasedoninductivelearningisthatitdoesnotrequiretheuseofatheoremprover.Thisisparticularlybeneficialinoursettingbecauseourlogicisundecidable.nnThepaperisorganizedasfollows:§2introducestermi-x185nologyandnotation.ReadersfamiliarwithTVLAcanskipto§2.2,whichbrieflysummarizesILP.§3illustratesourgoalsFig.1.Apossiblestoreforontheproblemofverifyingthepartialcorrectnessofasort-alinkedlist.ingroutine.§4describesthetechniquesusedforlearningabstractions.(Furtherdetailscanbefoundin[16].)§5presentsexperimentalresults.§6discussesrelatedwork.2Background

IntendedMeaningDov1andv2denotethesamememorycell?Doespointervariableqpointtomemorycellv?Doesthenfieldofv1pointtov2?Isthedatafieldofv1lessthanorequaltothatofv2?(b)2.1StoresasLogicalStructuresandtheirAbstractionsRelationtypedefstructnode{eq(v1,v2)structnode*n;

q(v)intdata;

n(v1,v2)}*List;

dle(v1,v2)(a)

Table1.(a)Declarationofalinked-listdatatypeinC.(b)CorerelationsusedforrepresentingthestoresmanipulatedbyprogramsthatusetypeList.Ourworkextendsthe

tn,dleprogram-analysisframework

u1n,tnu2n,tnu3of[21].Inthatapproach,xrn,xrn,xrn,xdledleconcretememoryconfigura-tn,dletn,dletn,dletions(i.e.,stores)areencoded

xrn,xcnnu1u2u3tnu1u2u3dleu1u2u3aslogicalstructuresinterms

u1110u1010u1111u1111ofafixedcollectionofcoreu2010u2001u2011u2010relations,C.Corerelationsu3010u3000u3001u3011arepartoftheunderlying

semanticsofthelanguagetoFig.2.AlogicalstructureS2thatrepresentsthestoreshownbeanalyzed.Forinstance,inFig.1ingraphicalandtabularforms.Tab.1givesthedefinitionofaClinked-listdatatype,andliststherelationsthatwouldbeusedtorepresentthestoresmanipulatedbyprogramsthatusetypeList,suchasthestoreinFig.1.2-valuedlogicalstructuresthenrepresentmemoryconfigurations:theindividualsarethesetofmemorycells;inthisexample,unaryrelationsrepresentpointervariablesandbinaryrelationnrepresentsthen-fieldofaListcell.Thedatafieldismodeledindirectly,viathebinaryrelationdle(whichstandsfor“data2less-than-or-equal-to”)listedinTab.1.Fig.2shows2-valuedstructureS2,whichrepresentsthestoreofFig.1(relationstn,rn,x,andcnwillbeexplainedbelow).

LetR={eq,p1,...,pn}beafinitevocabularyofrelationsymbols,whereRkde-notesthesetofrelationsymbolsofarityk(andeq∈R2).A2-valuedlogicalstructureSoverRisasetofindividualsUS,alongwithaninterpretationthatmapseachrelationsymbolpofarityktoatruth-valuedfunction:pS:(US)k→{0,1},whereeqSistheequalityrelationonindividuals.Thesetof2-valuedstructuresisdenotedbyS2[R].In3-valuedlogic,athirdtruthvalue—1/2—isintroducedtodenoteuncertainty.Forl1,l2∈{0,1/2,1},theinformationorderisdefinedasfollows:l1⊑l2iffl1=l2orl2=1/2.A3-valuedlogicalstructureSisdefinedlikea2-valuedlogicalstruc-ture,exceptthatthevaluesinrelationscanbe{0,1/2,1}.AnindividualforwhicheqS(u,u)=1/2iscalledasummaryindividual.Asummaryindividualabstractsoneormorefragmentsofadatastructure,andcanrepresentmorethanoneconcretemem-orycell.Thesetof3-valuedstructuresisdenotedbyS3[R].

ConcreteandAbstractSemanticsAconcreteoperationalsemanticsisdefinedbyspecifyingastructuretransformerforeachkindofedgeethatcanappearinatransitionsystem.Astructuretransformerisspecifiedbyprovidingrelation-updateformulasforthecorerelations.3Theseformulasdefinehowthecorerelationsofa2-valuedlogicalstructureSthatarisesatthesourceofearetransformedbyetocreatea2-valuedlogicalstructureS′atthetargetofe.Edgeemayoptionallyhaveapreconditionformula,whichfiltersoutstructuresthatshouldnotfollowthetransitionalonge.

However,setsof2-valuedstructuresdonotyieldasuitableabstractdomain;forinstance,whenthelanguagebeingmodeledsupportsallocationfromtheheap,thesetofindividualsthatmayappearinastructureisunbounded,andthusthereisnoaprioriupperboundonthenumberof2-valuedstructuresthatmayariseduringtheanalysis.Toensuretermination,weabstractsetsof2-valuedstructuresusing3-valuedstruc-tures.Asetofstoresisthenrepresentedbya(finite)setof3-valuedlogicalstructures.Theabstractionisdefinedusinganequivalencerelationonindividuals:eachindivid-ualofa2-valuedlogicalstructure(representingaconcretememorycell)ismappedtoanindividualofa3-valuedlogicalstructureaccordingtothevectorofvaluesthattheconcreteindividualhasforauser-chosencollectionofunaryabstractionrelations:Definition(CanonicalAbstraction).LetS∈S2,andletA⊆R1besomechosensubsetoftheunaryrelationsymbols.TherelationsinAarecalledabstractionrelations;theydefinethefollowingequivalencerelation≃AonUS:

u1≃Au2⇐⇒forallp∈A,pS(u1)=pS(u2),

andthesurjectivefunctionfA:US→US/≃A,suchthatfA(u)=[u]≃A,whichmapsanindividualtoitsequivalenceclass.ThecanonicalabstractionofSwithre-specttoA(denotedbyfA(S))performsthejoin(intheinformationorder)ofpredicatevalues,therebyintroducing1/2’s.2

Ifallunaryrelationsareabstractionrelations(A=R1),thecanonicalabstractionof2-valuedlogicalstructureS2isS3,showninFig.3,withfA(u1)=u1andfA(u2)=

3

Formulasarefirst-orderformulaswithtransitiveclosure:aformulaoverthevocabularyRisdefinedasfollows(wherep∗(v1,v2)standsforthereflexivetransitiveclosureofp(v1,v2)):p∈R,ϕ::=0|1|p(v1,...,vk)|(¬ϕ1)|(v1=v2)ϕ∈Formulas,|(ϕ1∧ϕ2)|(ϕ1∨ϕ2)|(ϕ1→ϕ2)|(ϕ1↔ϕ2)v∈Variables|(∃v:ϕ1)|(∀v:ϕ1)|p∗(v1,v2)

3

fA(u3)=u23.S3representsalllistswithtwoormoreelements,inwhichthefirstelement’sdatavalueislowerthanthedatavaluesintherestofthelist.Thefollowinggraphicalnotationisusedfordepicting3-valuedlogicalstructures:

–Individualsarerepresentedbycirclescontainingtheirnamesand(non-0)valuesforunaryrelations.Summaryindividualsarerepresentedbydoublecircles.

–Aunaryrelationpcorrespondingtoapointer-valuedprogramvariableisrepre-sentedbyasolidarrowfromptotheindividualuforwhichp(u)=1,andbytheabsenceofap-arrowtoeachnodeu′forwhichp(u′)=0.(Ifp=0forallindividuals,therelationnamepisnotshown.)

–Abinaryrelationqisrepresentedbyasolidarrowlabeledqbetweeneachpairofindividualsuiandujforwhichq(ui,uj)=1,andbytheabsenceofaq-arrow

′′′

betweenpairsu′iandujforwhichq(ui,uj)=0.

–Relationswithvalue1/2arerepresentedbydottedarrows.Canonicalabstractionensuresu1tn,dleu23thateach3-valuedstructureisxrn,xrn,xnnolargerthansomefixedsize,tn,dlen,tn,dleknownapriori.Moreover,thexrn,xcnnu1u23tnu1u23dleu1u23meaningofagivenformulainu1110u101/2u111u111theconcretedomain(℘(S2))isu23010u2301/2u2301/2u2301/2consistentwithitsmeaningintheabstractdomain(℘(S3)),al-Fig.3.A3-valuedstructureS3thatisthecanonicalab-thoughtheformula’svalueinanstractionofstructureS2.abstractstructurefA(S)maybelessprecisethanitsvalueintheconcretestructureS.Abstractinterpretationcollectsasetof3-valuedstructuresateachprogrampoint.Itcanbeimplementedasaniterativeprocedurethatfindstheleastfixedpointofacertaincollectionofequationsonvariablesthattaketheirvaluesin℘(S3)[21].pIntendedMeaningψptn(v1,v2)Isv2reachablefromv1alongnfields?n∗(v1,v2)rn,x(v)Isvreachablefrompointervariablex∃v1:x(v1)∧tn(v1,v)alongnfields?cn(v)Isvonadirectedcycleofnfields?∃v1:n(v1,v)∧tn(v,v1)Table2.Definingformulasofsomecommonlyusedinstrumentationrelations.Thereisaseparate

reachabilityrelationrn,xforeveryprogramvariablex.

InstrumentationRelationsTheabstractionfunctiononwhichananalysisisbased,andhencetheprecisionoftheanalysisdefined,canbetunedby(i)choosingtoequipstructureswithadditionalinstrumentationrelationstorecordderivedproperties,and(ii)varyingwhichoftheunarycoreandunaryinstrumentationrelationsareusedasthesetofabstractionrelations.ThesetofinstrumentationrelationsisdenotedbyI.Eachrelationsymbolp∈Ik⊆Rkisdefinedbyaninstrumentation-relationdefinitionformulaψp(v1,...,vk).Instrumentationrelationsymbolsmayappearinthedefiningformulasofotherinstrumentationrelationsaslongastherearenocirculardependences.Theintroductionofunaryinstrumentationrelationsthatareusedasabstractionre-lationsprovidesawaytocontrolwhichconcreteindividualsaremergedtogether,andtherebycontroltheamountofinformationlostbyabstraction.Tab.2listssomeinstru-mentationrelationsthatareimportantfortheanalysisofprogramsthatusetypeList.

4

2.2InductiveLogicProgramming(ILP)

Givenalogicalstructure,thegoalofanILPalgorithmistolearnalogicalrelation(definedintermsofthelogicalstructure’sotherrelations)thatagreeswiththeclassi-ficationofinputexamples.ILPalgorithmsproducetheanswerintheformofalogicprogram.(Non-recursive)logicprogramscorrespondtoasubsetoffirst-orderlogic.4Alogicprogramcanbethoughtofasadisjunctionovertheprogramrules,witheachrulecorrespondingtoaconjunctionofliterals.Variablesnotappearingintheheadofaruleareimplicitlyexistentiallyquantified.

Definition(ILP).GivenasetofpositiveexampletuplesE+,asetofnegativeex-ampletuplesE−,andalogicalstructure,thegoalofILPistofindaformulaψEsuchthatalle∈E+aresatisfied(orcovered)byψEandnoe∈E−issatisfiedbyψE.2

Forexample,considerlearningaunaryformulathatu1u3u4u5holdsforlinked-listelementsthatarepointedtobythen

u2fieldsofmorethanoneelement(asusedin[11,3]).We

+−2-valuedFig.4.AlinkedlistwithletE={u3,u5}andE={u1,u4}inthedefstructureofFig.4.TheformulaψisShared(v)=∃v1,v2:sharedelements.n(v1,v)∧n(v2,v)∧¬eq(v1,v2)meetstheobjective,as

itcoversallpositiveandnonegativeexampletuples.Fig.5presentstheILPrelationE(v1,...,vk),algorithmusedbysystemsInput:TargetStructureS∈S3[R],suchasFOIL[19],modi-SetoftuplesPos,SetoftuplesNegfiedtoconstructtheanswer[1]ψE:=0while(Pos=∅)asafirst-orderlogicfor-[2][3]NewDisjunct:=1mulaindisjunctivenormal[4]NewNeg:=Negform.Thisalgorithmisca-[5]while(NewNeg=∅)Cand:=candidateliteralsusingRpableoflearningthefor-[6][7]Best:=L∈CandwithmaxGain(L,NewDisjunct)

mulaψisShared(v)(byper-[8]NewDisjunct:=NewDisjunct∧LNewNeg:=subsetofNewNegsatisfyingLformingoneiterationofthe[9][10]∃-quantifyNewDisjunctvariables∈/{v1,...,vk}

outerloopandthreeiter-[11]ψ:=ψ∨NewDisjunctEEationsoftheinnerloop[12]Pos:=subsetofPosnotsatisfyingNewDisjuncttosuccessivelychooselit-Fig.5.Pseudo-codeforFOIL.eralsn(v1,v),n(v2,v),and¬eq(v1,v2)).ItisasequentialcoveringalgorithmparameterizedbythefunctionGain,whichcharacterizestheusefulnessofaddingaparticularliteral(generally,insomeheuristicfashion).Thealgorithmcreatesanewdisjunctaslongastherearepositiveexamplesthatarenotcoveredbyexistingdisjuncts.Thedisjunctisextendedbycon-joininganewliteraluntilitcoversnonegativeexamples.EachliteralusesarelationsymbolfromthevocabularyofstructureS;validargumentstoaliteralarethevariablesoftargetrelationE,aswellasnewvariables,aslongasatleastoneoftheargumentsisavariablealreadyusedinthecurrentdisjunct.InFOIL,oneliteralischosenusingaheuristicvaluebasedontheinformationgain(seeline[7]).FOILusesinformationgaintofindtheliteralthatdifferentiatesbestbetweenpositiveandnegativeexamples.

3

4

Example:VerifyingSortedness

ILPalgorithmsarecapableofproducingrecursiveprograms,whichcorrespondtofirst-orderlogicplusaleast-fixpointoperator(whichismoregeneralthantransitiveclosure).

5

Giventhestatic-analysisalgorithmdefinedin§2.1,todemonstratethepartialcorrectnessofaproce-dure,theusermustsupplythefollowingprogram-specificinformation:

–Theprocedure’scontrol-flowgraph.

–Adata-structureconstructor(DSC):acodefragmentthatnon-deterministicallyconstructsallvalidinputs.

–Aquery;i.e.,aformulathatidentifiesthein-tendedoutputs.

TheanalysisalgorithmisrunontheDSCconcate-natedwiththeprocedure’scontrol-flowgraph;thequeryisthenevaluatedonthestructuresthataregeneratedatexit.

ConsidertheproblemofestablishingthatInsertSortshowninFig.6ispartiallycorrect.Thisisanassertionthatcomparesthestateofastoreattheendofaprocedurewithitsstateatthestart.Inparticular,acorrectsortingroutinemustperformapermutationoftheinputlist,i.e.alllistelementsreachablefromvariablexatthestartoftheroutinemustbereachablefromxattheend.Wecanexpressthepermutationpropertyasfollows:

[1]voidInsertSort(Listx){[2]Listr,pr,rn,l,pl;[3]r=x;

[4]pr=NULL;

[5]while(r!=NULL){[6]l=x;

[7]rn=r->n;[8]pl=NULL;

[9]while(l!=r){[10]if(l->data>r->data){[11]pr->n=rn;[12]r->n=l;[13]if(pl==NULL)x=r;[14]elsepl->n=r;[15]r=pr;[16]break;[17]}[18]pl=l;[19]l=l->n;[20]}

[21]pr=r;[22]r=rn;[23]}[24]}

Fig.6.Astableversionofinsertionsort.

0

∀v:rn,x(v)↔rn,x(v),

(1)

0

wherern,xdenotesthereachabilityrelationforxatthebeginningofInsertSort.IfFormula(1)holds,thentheelementsreachablefromxafterInsertSortexecutesareexactlythesameasthosereachableatthebeginning,andconsequentlytheprocedureperformsapermutationoflistx.Ingeneral,foreachrelationp,wehavesuchahistoryrelationp0.

Fig.7showsthethreestructuresthatcharacterizethevalidinputstoInsertSort(theyrepresentthesetofstoresinwhichprogramvariablexpointstoanacycliclinkedlist).ToverifythatInsertSortproducesasortedpermutationoftheinputlist,wewouldchecktoseewhether,forallofthestructuresthatariseattheprocedure’sexitnode,thefollowingformulaevaluatesto1:

∀v1:rn,x(v1)→(∀v2:n(v1,v2)→dle(v1,v2)).(2)

Ifitdoes,thenthenodesreachablefromxmustbeinnon-decreasingorder.

Abstractinterpretationcollects3-valuedstructureS3showninFig.3atline[24].NotethatFormula(2)evaluatesto1/2onS3.Whilethefirstlistelementisguaranteedtobeincorrectorderwithrespecttotheremainingelements,thereisnoguaranteethatalllistnodesrepresentedbythesummarynodeareincorrectorder.Inparticular,becauseS3representsS2,showninFig.2,theanalysisadmitsthepossibilitythatthe(correct)implementationofinsertionsortofFig.6canproducethestoreshowninFig.1.Thus,theabstractionthatweusedwasnotfine-grainedenoughtoestablishthepartialcorrectnessofInsertSort.Infact,theabstractionisnotfine-grainedenoughtoseparatethesetofsortedlistsfromthelistsnotinsortedorder.

6

In[15],Lev-Amietal.usedTVLAtoestablishthepartialcorrectnessofInsertSort.ThekeystepwastheintroductionofinstrumentationrelationinOrderdle,n(v),whichholdsfornodeswhosedata-componentsarelessthanorequaltothoseoftheirn-successors;inOrderdle,n(v)wasdefinedby:

inOrderdle,n(v)=∀v1:n(v,v1)→dle(v,v1).

Thesortednesspropertywasthenstatedasfollows(cf.Formula(2)):

∀v:rn,x(v)→inOrderdle,n(v).

(4)

def

(3)

Aftertheintroductionofrelationemptylist1-elementlistlistswith2ormoreelementsinOrderdle,n,the3-valuedstructuresthatdlenrrrxxarecollectedbyabstractinterpretationatn,xn,xn,xtntheendofInsertSortdescribealltn,dletn,dlen,tn,dlestoresinwhichvariablexpointstoan

acyclic,sortedlinkedlist.InalloftheseFig.7.Thestructuresthatdescribepossiblein-structures,Formulas(4)and(1)evaluateputstoInsertSort.to1.Consequently,InsertSortisguaranteedtoworkcorrectlyonallvalidinputs.4LearninganAbstraction

In[15],instrumentationrelationinOrderdle,nwasdefinedexplicitly(bytheTVLAuser).Heretofore,therehavereallybeentwoburdensplacedontheTVLAuser:(i)hemusthaveinsightintothebehavioroftheprogram,and(ii)hemusttranslatethisinsightintoappropriateinstrumentationrelations.Thegoalofthispaperistoauto-Input:atransitionsystem,matetheidentificationofappropri-adata-structureconstructor,aqueryϕ(aclosedformula)ateinstrumentationrelations,such

asinOrderdle,n.ForInsertSort,[1]Constructabstractinputthegoalistoobtaindefiniteanswers[2]doPerformabstractinterpretationwhenevaluatingFormula(2)onthe[3]

[4]LetS1,...,Skbethesetofstructurescollectedbyabstractin-3-valuedstructuresatexit

terpretationatline[24]ofFig.6.[5]i

ifforallSi,[[ϕ]]S3([])=1/2break

Fig.8givespseudo-codeforour[6]Findformulasψp1,...,ψpkfornewmethod,thestepsofwhichcanbeinstrumentationrelsp1,...,pk

[7]Refinetheactionsthatdefineexplainedasfollows:

thetransitionsystem–(Line[1];[16,§4.3])Use

Refinetheabstractinputadata-structureconstructorto[8]

computetheabstractinputstruc-[9]while(true)

turesthatrepresentallvalidin-Fig.8.Pseudo-codeforiterativeabstractionrefine-ment.putstotheprogram.

–Performanabstractinterpretationtocollectasetofstructuresateachprogrampoint,andevaluatethequeryonthestructuresatexit.Ifadefiniteanswerisobtainedonallstructures,terminate.Otherwise,performabstractionrefinement.

–(Line[6];§4.1and§4.2)Finddefiningformulasfornewinstrumentationrelations.–(Line[7])Replacealloccurrencesoftheseformulasinthequeryandinthedef-initionsofotherinstrumentationrelationswiththeuseofthecorrespondingnewinstrumentationrelationsymbols,andapplyfinitedifferencing[20]togeneratere-finedrelation-updateformulasforthetransitionsystem.

7

–(Line[8];[16,§4.3])Obtainthemostprecisepossiblevaluesforthenewlyintro-ducedinstrumentationrelationsinabstractstructuresthatdefinethevalidinputstotheprogram.Thisisachievedby“reconstructing”thevalidinputsbyperformingabstractinterpretationofthedata-structureconstructor.

Afirstattemptatabstractionrefinementcouldbetheintroductionofthequeryitselfasanewinstrumentationrelation.However,thisusuallydoesnotleadtoadefiniteanswer.Forinstance,withInsertSort,introducingthequeryasanewinstrumentationre-lationisineffectivebecausenostatementoftheprogramhastheeffectofchangingthevalueofsuchaninstrumentationrelationfrom1/2to1.

Incontrast,whenunaryinstrumentationrelationinOrderdle,nispresent,thereareseveralstatementsoftheprogramwhereabstractinterpretationresultsinnewdefiniteentriesforinOrderdle,n.Forinstance,becauseofthecomparisoninline[10]ofFig.6,theinsertioninlines[12]–[14]ofthenodepointedtobyr(sayu)beforethenodepointedtobylresultsinanewdefiniteentryinOrderdle,n(u).

Analgorithmtogeneratenewinstrumentationrelationsshouldtakeintoaccountthesourcesofimprecision.§4.1describessubformula-basedrefinement;§4.2describesILP-basedrefinement.Atpresent,weemploysubformula-basedrefinementfirst,be-causethecostofthisstrategyisreasonable(see§5)andthestrategyisoftensuccessful.Whensubformula-basedrefinementcannolongerrefinetheabstraction,weturntoILP.BecauseaqueryhasfinitelymanysubformulasandwecurrentlylimitourselvestooneroundofILP-basedrefinement,thenumberofabstraction-refinementstepsisfinite.Because,additionally,eachrunoftheanalysisexploresaboundednumberof3-valuedstructures,thealgorithmisguaranteedtoterminate.4.1Subformula-BasedRefinement

Whenthequeryϕevaluatesto1/2onastructureScollectedattheexitnode,weinvokefunctioninstrum,arecursive-descentproceduretogeneratedefiningformulasfornewinstrumentationrelationsbasedonthesubformulasofϕresponsiblefortheimprecision.Thedetailsoffunctioninstrumaregivenin[16,§4.1].

Example.Aswesawin§3,abstractinterpretationcollects3-valuedstructureS3ofFig.3attheexitnodeofInsertSort.Thesortednessquery(Formula(2))eval-uatesto1/2onS3,triggeringacalltoinstrumwithFormula(2)andstructureS3,asarguments.Column2ofTab.3showstheinstrumentationrelationsthatarecreatedasaresultofthecall.Notethatsorted3isdefinedexactlyasinOrderdle,n,whichwasthekeyinsightfortheresultsof[15].2

psorted1()sorted2(v1)sorted3(v1)sorted4(v1,v2)ψp(aftercalltoinstrum)∀v1:rn,x(v1)→(∀v2:n(v1,v2)→dle(v1,v2))rn,x(v1)→(∀v2:n(v1,v2)→dle(v1,v2))∀v2:n(v1,v2)→dle(v1,v2)n(v1,v2)→dle(v1,v2)ψp(finalversion)∀v1:sorted2(v1)rn,x(v1)→sorted3(v1)∀v2:sorted4(v1,v2)n(v1,v2)→dle(v1,v2)Table3.Instrumentationrelationscreatedbysubformula-basedrefinement.

Theactionsthatdefinetheprogram’stransitionrelationneedtobemodifiedtogainprecisionimprovementsfromstoringandmaintainingthenewinstrumentationrela-tions.Toaccomplishthis,refinementoftheprogram’sactions(line[7]inFig.8)re-placesalloccurrencesofthedefiningformulasforthenewinstrumentationrelationsin

8

thequeryandinthedefinitionsofotherinstrumentationrelationswiththeuseofthecorrespondingnewinstrumentation-relationsymbols.

Example.ForInsertSort,theuseofFormula(2)inthequeryisreplacedwiththeuseofthestoredvaluesorted1().Thenthedefinitionsofallinstrumentationre-lationsarescannedforoccurrencesofψsorted1,...,ψsorted4.Theseoccurrencesarereplacedwiththenamesofthefourrelations.Inthiscase,onlythenewrelations’defi-nitionsarechanged,yieldingthedefinitionsgiveninColumn3ofTab.3.

InallofthestructurescollectedattheexitnodeofInsertSortbythesecondrunofabstractinterpretation,sorted1()=1.Thepermutationpropertyalsoholdsonallofthestructures.ThesetwofactsestablishthepartialcorrectnessofInsertSort.Thisprocessrequiredoneiterationofabstractionrefinement,usedthebasicversionofthespecification(thevocabularyconsistedoftherelationsofTabs.1and2,togetherwiththecorrespondinghistoryrelations),andneedednouserintervention.2

4.2ILP-BasedRefinement

ShortcomingsofSubformula-BasedRefinementToillustrateaweaknessinsubformula-basedrefinement,weintroducethestabilityproperty.Thestabilityprop-ertyusuallyarisesinthecontextofsortingprocedures,butactuallyappliestolist-manipulatingprogramsingeneral:thestabilityquery(Formula(5))assertsthattherelativeorderofelementswithequaldata-componentsremainsthesame.5

∀v1,v2:(dle(v1,v2)∧dle(v2,v1)∧t0n(v1,v2))→tn(v1,v2)

(5)

ProcedureInsertSortconsistsoftwonestedloops(seeFig.6).Theouterloop

traversesthelist,settingpointervariablertopointtolistnodes.Foreachiterationoftheouterloop,theinnerloopfindsthecorrectplacetoinsertr’starget,bytraversingthelistfromthestartusingpointervariablel;r’stargetisinsertedbeforel’stargetwhenl->data>r->data.BecauseInsertSortsatisfiestheinvariantthatalllistnodesthatappearinthelistbeforer’stargetarealreadyinthecorrectorder,thedata-componentofr’stargetislessthanthedata-componentofallnodesaheadofwhichr’stargetismoved.Thus,InsertSortpreservestheoriginalorderofelementswithequaldata-components,andInsertSortisastableroutine.

However,subformula-basedrefinementisnotcapableofestablishingthestabilityofInsertSort.Byconsideringonlysubformulasofthequery(inthiscase,For-mula(5))ascandidateinstrumentationrelations,thestrategyisunabletointroduceinstrumentationrelationsthatmaintaininformationaboutthetransitivesuccessorswithwhichalistnodehasthecorrectrelativeorder.

LearningInstrumentationRelationsFig.9showsthestructureS9,whicharisesdur-ingabstractinterpretationjustbeforeline[6]ofFig.6,togetherwithatabularversionofrelationstnanddle.(Weomitreachabilityrelationsfromthefigureforclarity.)Af-tertheassignmentl=x;,nodesu2andu3haveidenticalvectorsofvaluesfortheunaryabstractionrelations.Thesubsequentapplicationofcanonicalabstractionpro-ducesstructureS10,showninFig.10.BoldentriesoftablesinFig.9indicatedefinite

5

Arelatedproperty,antistability,assertsthattheorderofelementswithequaldata-componentsisreversed:∀v1,v2:(dle(v1,v2)∧dle(v2,v1)∧t0n(v1,v2))→tn(v2,v1)OurtestsuitealsoincludesprogramInsertSortAS,whichisidenticaltoInsertSortexceptthatituses≥insteadof>inline[10]ofFig.6(i.e.,whenlookingforthecorrectplacetoinsertthecurrentnode).Thisimplementationofinsertionsortisantistable.

9

valuesthataretransformedinto1/2inS10.StructureS9satisfiesthesortednessinvari-antdiscussedabove:everynodeamongu1,...,u4hasthedlerelationshipwithallnodesappearinglaterinthelist,exceptr’starget,u5.However,apieceofthisinformationislostinstructureS10:dle(u23,u23)=1/2,indicatingthatsomenodesrepresentedbysummarynodeu23mightnotbeinsortedorderwithrespecttotheirsuccessors.Wewillrefertosuchabstractionstepsasinformation-losspoints.Anabstractstructuretransformer

lprx,plr,rnmaytemporarilycreateastructureS1

thatisnotintheimageofcanonical

u1n,dleu2n,dleu3n,dleu4nu5abstraction[21].Thesubsequentappli-cationofcanonicalabstractiontrans-dleu1u2u3u4u5tnu1u2u3u4u5formsS1intostructureS2bygrouping

u111111/2u111111asetU1oftwoormoreindividualsofu21/21111/2u201111S1intoasinglesummaryindividualofu300111/2u300111u4001/211/2u400011S2.Thelossofprecisionisduetoone

u51/21/21/21/21u500001orbothofthefollowingcircumstances:

–OneoftheindividualsinU1pos-Fig.9.StructureS9,whicharisesjustbeforesessesapropertythatanotherindi-line[6]ofFig.6.Unlabelededgesbetweennodesvidualdoesnotpossess;thus,therepresentthedlerelation.propertyforthesummaryindividualis1/2.–IndividualsinU1haveapropertyincommon,whichcannotberecomputedpre-ciselyinS2.

n,dlex,pl,lprr,rnInbothcases,thesolutionliesintheintroduc-nnunutionofnewinstrumentationrelations.Inthefor-u5u1423mercase,itisnecessarytointroduceaunaryab-dleu1u23u4u5tnu1u23u4u5stractionrelationtokeeptheindividualsofU1u11111/2u11111thatpossessthepropertyfrombeinggroupedu231/21/211/2u2301/211withthosethatdonot.Inthelattercase,itisu401/211/2u40011u51/21/21/21u50001sufficienttointroduceanon-abstractionrelationofappropriatearitythatcapturesthecommonFig.10.StructureS10,correspondingtopropertyofindividualsinU1.Thealgorithmde-thetransformationofS9bythestatementscribedin§2.2canbeusedtolearnformulasforonline[6]ofFig.6.Unlabelededgesbe-tweennodesrepresentthedlerelation.thefollowingthreekindsofrelations:6

+

TypeI:Unaryrelationr1withE={u}foroneu∈U1,andE−=U1−{u}.TypeII:Unaryrelationr2withE+=U1.TypeIII:Binaryrelationr3withE+=U1×U1.TypeIrelationsareintendedtopreventthegroupingofindividualswithdifferentproperties,whileTypesIIandIIIareintendedtocapturethecommonpropertiesofindividualsinU1.(TypeIIIrelationscanbegeneralizedtohigher-arityrelations.)ForthelogicalstructurethatservesasinputtoILP,wepassthestructureS1iden-tifiedataninformation-losspoint.Werestrictthealgorithmtouseonlynon-history6

Thesearewhatareneededforouranalysisframework,whichusesabstractionsthatgeneralizepredicate-abstractiondomains.AfourthuseofILPprovidesanewtechniqueforpredicateabstractionitself:ILPcanbeusedtoidentifynullaryrelationsthatdifferentiateapositive-examplestructureSfromtheotherstructuresarisingataprogrampoint.ThestepsofILPgobeyondmerelyformingBooleancombinationsofexistingrelations;theyinvolvethecreationofnewrelationsbyintroducingquantifiersduringthelearningprocess.

10

relationsofthestructurethatlosedefiniteentriesasaresultofabstraction(e.g.,tnanddleintheaboveexample).Definiteentriesofthoserelationsarethenusedtolearnfor-mulasthatevaluateto1foreverypositiveexampleandto0foreverynegativeexample.Wemodifiedthealgorithmof§2.2tolearnmultipleformulasinoneinvocationofthealgorithm.Ourmotivationisnottofindasingleinstrumentationrelationthatexplainssomethingaboutthestructure,butrathertofindallinstrumentationrelationsthathelptheanalysisestablishthepropertyofinterest.Wheneverwefindmultipleliteralsofthesamequality(seeline[7]ofFig.5),weextenddistinctcopiesofthecurrentdisjunctusingeachoftheliterals,andthenweextenddistinctcopiesofthecurrentformulausingtheresultingdisjuncts.

ThisvariantofILPisabletolearnausefulbinaryformulausingstructureS9ofFig.9.ThesetofindividualsofS9thataregroupedbytheabstractionisU={u2,u3},sotheinputsetofpositiveexamplesis{(u2,u2),(u2,u3),(u3,u2),(u3,u3)}.Thesetofrelationsthatlosedefinitevaluesduetoabstractionincludestnanddle.Literaldle(v1,v2)coversthreeofthefourexamplesbecauseitholdsforbindings(v1,v2)→(u2,u2),(v1,v2)→(u2,u3),and(v1,v2)→(u3,u3).Thealgorithmpicksthatliteraland,becausetherearenonegativeexamples,dle(v1,v2)becomesthefirstdisjunct.Lit-eral¬tn(v1,v2)coverstheremainingpositiveexample,(u3,u2),andthealgorithmreturnstheformula

def

ψr3(v1,v2)=dle(v1,v2)∨¬tn(v1,v2),(6)whichcanbere-writtenastn(v1,v2)→dle(v1,v2).

Relationr3allowstheabstractiontomaintaininformationaboutthetransitivesuc-cessorswithwhichalistnodehasthecorrectrelativeorder.Inparticular,althoughdle(u23,u23)is1/2inS10,r3(u23,u23)is1,whichallowsestablishingthefactthatalllistnodesappearingpriortor’stargetareinsortedorder.

Otherformulas,suchasdle(v1,v2)∨tn(v2,v1),arealsolearnedusingILP(cf.Fig.12).Notallofthemareusefultotheverificationprocess,butintroducingextrainstrumentationrelationscannotharmtheanalysis,asidefromincreasingitscost.

5ExperimentalEvaluation

WeextendedTVLAtoperformiterativeabstractionrefinement,andappliedittothreequeriesandfiveprograms(seeFig.11).BesidesInsertSort,thetestprogramsin-cludedsortingproceduresBubbleSortandInsertSortAS,list-mergingproce-dureMerge,andin-situlist-reversalprocedureReverse.

Atpresent,weemploysubformula-basedrefinementfirst.Duringeachiterationofsubformula-basedrefinement,wesavelogicalstructuresatinformation-losspoints.Uponthefailureofsubformula-basedrefinement,weinvoketheILPalgorithmde-scribedin§4.2.Tolowerthecostoftheanalysisweprunethereturnedsetoffor-mulas.Forexample,wecurrentlyremoveformulasdefinedintermsofasinglerelationsymbol;suchformulasareusuallytautologies(e.g.,dle(v1,v2)∨dle(v2,v1)).Wethendefinenewinstrumentationrelations,andusetheserelationstorefinetheabstractionbyperformingthestepsoflines[7]and[8]ofFig.8.Ourimplementationcanlearnrela-tionsofalltypesdescribedin§4.2:unary,binary,aswellasnullary.However,duetothepresentcostofmaintainingmanyunaryinstrumentationrelationsinTVLA,intheexperimentsreportedhereweonlylearnbinaryformulas(i.e.,ofTypeIII).Moreover,wedefinenewinstrumentationrelationsusingonlylearnedformulasofasimpleform

11

(currently,thosewithtwoatomicsubformulas).Weareintheprocessofextendingourtechniquesforpruninguselessinstrumentationrelations.ThisshouldmakeitpracticalforustousealltypesofrelationsthatcanbelearnedbyILPforrefiningtheabstraction.Example.WhenattemptingtoverifythestabilityofInsertSort,ILPcreatesnineformulasincludingFormula(6).ThesubsequentrunoftheanalysissuccessfullyverifiesthestabilityofInsertSort.2

Fig.11showsthatthemethodwasabletogen-TestProgramsortedstableantistableeratetherightinstrumentationrelationsforTVLA

BubbleSort111/2toestablishallpropertiesthatweexpecttohold.InsertSort111/2Namely,TVLAsucceedsindemonstratingthatInsertSortAS11/21Merge1/211/2allthreesortingroutinesproducesortedlists,thatReverse1/21/21BubbleSort,InsertSort,andMergeare

Fig.11.Resultsfromapplyingitera-stableroutines,andthatInsertSortASandtiveabstractionrefinementtotheveri-Reverseareantistableroutines.ficationofpropertiesofprogramsthatIndefiniteanswersareindicatedby1/2en-manipulatelinkedlists.tries.Itisimportanttounderstandthatalloftheoccurrencesof1/2inFig.11arethemostprecisecorrectanswers.Forinstance,theresultofapplyingReversetoanunsortedlistisusuallyanunsortedlist;however,inthecasethattheinputlisthappenstobeinnon-increasingorder,Reverseproducesasortedlist.Consequently,themostpreciseanswertothequeryis1/2,not0.

Fig.12showsthenumbersofinstru-sortedstableantistablementationrelationsusedduringthelastTestProgram#instrumrels#instrumrels#instrumrelstotal/ILPtotal/ILPtotal/ILPiterationofabstractionrefinement.The

BubbleSort31/032/041/9numberofILP-learnedrelationsusedbyInsertSort39/049/943/3theanalysisissmallrelativetothetotalInsertSortAS39/043/340/0numberofinstrumentationrelations.Merge30/328/031/3Reverse26/327/324/0Fig.13givesexecutiontimesthatFig.12.Thenumbersofinstrumentationrela-werecollectedona3GHzLinuxPC.Thetions(totalandlearnedbyILP)usedduringthelongest-runninganalysis,whichverifieslastiterationofabstractionrefinement.thatInsertSortisstable,takes8.5minutes.Sevenoftheanalysestakeunderaminute.Theresttakebetween70sec-ondsand6minutes.Thetotaltimeforthe15testsis35minutes.Thesenumbersareveryclosetohowlongittakestoverifythesortednessquerieswhentheusercarefullychoosestherightinstrumentationrelations[15].7Themaximumamountofmemoryusedbytheanalysesvariedfromjustunder2MBto32MB.8

ThecostoftheinvocationsoftheILPalgorithmwhenattemptingtoverifytheantistabilityofBubbleSortwas25seconds(total,for133information-losspoints).Forallotherbenchmarks,theILPcostwaslessthantenseconds.

Threeadditionalexperimentstestedtheapplicabilityofourmethodtootherqueriesanddatastructures.Inthefirstexperiment,subformula-basedrefinementsuccessfullyverifiedthatthein-situlist-reversalprocedureReverseindeedproducesalistthatisthereversaloftheinputlist.Thequerythatexpressesthispropertyis∀v1,v2:n(v1,v2)↔n0(v2,v1).Thisexperimenttookonly5secondsandusedlessthan2MBofmemory.Thesecondandthirdexperimentsinvolvedtwoprogramsthatmanipu-78

SortednessistheonlyqueryinoursettowhichTVLAhasbeenappliedbeforethiswork.TVLAiswritteninJava.Herewereportthemaximumoftotalmemoryminusfreememory,asreturnedbyRuntime.

12

latebinary-searchtrees.InsertBSTinsertsanewnodeintoabinary-searchtree,andDeleteBSTdeletesanodefromabinary-searchtree.Forbothprograms,subformula-basedrefinementsuccessfullyverifiedthequerythatthenodesofthetreepointedtobyvariabletremaininsortedorderattheendoftheprograms:

∀v1:rt(v1)→(∀v2:(left(v1,v2)→dle(v2,v1))∧(right(v1,v2)→dle(v1,v2)))

(7)

Theinitialspecificationsfortheanalysesincludedonlythreestandardinstrumentationrelations,similartothoselistedinTab.2.Relationrt(v1)fromFormula(7),forexam-ple,distinguishesnodesinthe(sub)treepointedtobyt.TheInsertBSTexperimenttook30secondsandusedlessthan3MBofmemory,whiletheDeleteBSTexperi-menttookapproximately10minutesandused37MBofmemory.6RelatedWork

350514Post-ILP iteration300TheworkreportedhereissimilarinspirittoPre-ILP iterationscounterexample-guidedabstractionrefinementsorted250stable[12,4,13,18,5,2,8,6].Akeydifferencebe-antistable200tweenthisworkandpriorworkinthemodel-150checkingcommunityistheabstractdomain:100priorworkhasusedabstractdomainsthatare50fixed,finite,CartesianproductsofBooleanval-ues(i.e.,predicate-abstractiondomains),and0BubbleInsertInsertMergeReversehencetheonlyrelationsintroducedarenullarySortSort ASrelations.OurworkappliestoaricherFig.13.Executiontimes.Foreachpro-classofabstractions—3-valuedstructures—gram,thethreebarsrepresentthethatgeneralizepredicate-abstractiondomains.sorted,stable,andantistablequeries.Theabstraction-refinementalgorithmdescribedIncaseswheresubformula-basedrefine-inthispapercanintroduceunary,binary,mentfailed,theupperportionofthebarsternary,etc.relations,inadditiontonullaryre-showsthecostofthelastiterationofthelations.Whilewedemonstratedourapproachanalysis(onboththeDSCandthepro-usingshape-analysisqueries,thisapproachisgram)togetherwiththeILPcost.

applicableinanysettinginwhichfirst-orderlogicisusedtodescribeprogramstates.Aseconddistinguishingfeatureofourworkisthatthemethodisdrivennotbycoun-terexampletraces,butinsteadbyimpreciseresultsofevaluatingaquery(inthecaseofsubformula-basedrefinement)andbylossofinformationduringabstractionsteps(inthecaseofILP-basedrefinement).Theredonotcurrentlyexisttheoremproversforfirst-orderlogicextendedwithtransitiveclosurecapableofidentifyinginfeasibleerrortraces[9];henceweneededtodeveloptechniquesdifferentfromthoseusedinSLAM,BLAST,etc.SLAMidentifiestheshortestprefixofaspuriouscounterexampletracethatcannotbeextendedtoafeasiblepath;ingeneral,however,thefirstinformation-losspointoccursbeforetheendoftheprefix.Information-loss-guidedrefinementcaniden-tifytheearliestpointsatwhichinformationislostduetoabstraction,aswellaswhatnewinstrumentationrelationsneedtobeaddedtotheabstractionatthosepoints.Apo-tentialadvantageofcounterexample-guidedrefinementoverinformation-loss-guidedrefinementisthattheformerisgoal-driven.Information-loss-guidedrefinementcandiscovermanyrelationshipsthatdonothelpinestablishingthequery.Toalleviatethisproblem,werestrictedtheILPalgorithmtoonlyuserelationsthatoccurinthequery.

(seconds)13

Abstraction-refinementtechniquesfromtheabstract-interpretationcommunityarecapableofrefiningdomainsthatarenotbasedonpredicateabstraction.In[10],forexample,apolyhedra-baseddomainisdynamicallyrefined.Ourworkisbasedonadifferentabstractdomain,andledustodevelopsomenewapproachestoabstractionrefinement,basedonmachinelearning.

Intheabstract-interpretationcommunity,astrong(albeitoftenunattainable)formofabstractionrefinementhasbeenidentifiedinwhichthegoalistomakeabstractinterpre-tationcomplete(a.k.a.“optimal”)[7].Inourcase,thegoalistoextendtheabstractionjustenoughtobeabletoanswerthequery,ratherthantomaketheabstractionoptimal.

References

1.TVLAsystem.http://www.cs.tau.ac.il/tvla/.

2.T.BallandS.Rajamani.Automaticallyvalidatingtemporalsafetypropertiesofinterfaces.InSPIN,pages103–122,2001.

3.D.R.Chase,M.Wegman,andF.Zadeck.Analysisofpointersandstructures.InPLDI,pages296–310,1990.

4.E.M.Clarke,O.Grumberg,S.Jha,Y.Lu,andH.Veith.Counterexample-guidedabstractionrefinement.InCAV,pages1–169,2000.

5.S.DasandD.Dill.Counter-examplebasedpredicatediscoveryinpredicateabstraction.InFMCAD,pages19–32,2002.

6.C.Flanagan.Softwaremodelcheckingviaiterativeabstractionrefinementofconstraintlogicqueries.InCP+CV,2004.

7.R.Giacobazzi,F.Ranzato,andF.Scozzari.Makingabstractinterpretationscomplete.J.ACM,47(2):361–416,2000.

8.T.Henzinger,R.Jhala,R.Majumdar,andK.McMillan.Abstractionsfromproofs.InPOPL,pages232–244,2004.

9.N.Immerman,A.Rabinovich,T.Reps,M.Sagiv,andG.Yorsh.Theboundarybetweendecidabilityandundecidabilityfortransitiveclosurelogics.InCSL,pages160–174,2004.10.B.Jeannet,N.Halbwachs,andP.Raymond.Dynamicpartitioninginanalysesofnumerical

properties.InSAS,pages39–50,1999.

11.N.JonesandS.Muchnick.FlowanalysisandoptimizationofLisp-likestructures.InPro-gramFlowAnalysis:TheoryandApplications,pages102–131.Prentice-Hall,1981.

12.R.Kurshan.Computer-aidedVerificationofCoordinatingProcesses.PrincetonUniversity

Press,1994.

13.Y.Lakhnech,S.Bensalem,S.Berezin,andS.Owre.Incrementalverificationbyabstraction.

InTACAS,pages98–112,2001.14.N.LavraˇcandS.Dˇzeroski.InductiveLogicProgramming:TechniquesandApplications.

EllisHorwood,1994.

15.T.Lev-Ami,T.Reps,M.Sagiv,andR.Wilhelm.Puttingstaticanalysistoworkforverifica-tion:Acasestudy.InISSTA,pages26–38,2000.

16.A.Loginov,T.Reps,andM.Sagiv.Learningabstractionsforverifyingdata-structureprop-erties.reportTR-1519,Comp.Sci.Dept.,Univ.ofWisconsin,January2005.Availableat“http://www.cs.wisc.edu/wpis/papers/tr1519.ps”.

17.S.Muggleton.Inductivelogicprogramming.NewGenerationComp.,8(4):295–317,1991.18.C.Pasareanu,M.Dwyer,andW.Visser.Findingfeasiblecounter-exampleswhenmodel

checkingJavaprograms.InTACAS,pages284–298,2001.

19.J.R.Quinlan.Learninglogicaldefinitionsfromrelations.Mach.Learn.,5:239–266,1990.20.T.Reps,M.Sagiv,andA.Loginov.Finitedifferencingoflogicalformulaswithapplications

toprogramanalysis.InESOP,pages380–398,2003.

21.M.Sagiv,T.Reps,andR.Wilhelm.Parametricshapeanalysisvia3-valuedlogic.TOPLAS,

24(3):217–298,2002.

14