Detta papper beskriver en kompositionsform analys, där varje förfarande analyseras oberoende av dess anropare. Analysen använder en abstrakt domän baserad på ett begränsat fragment av separation logik, och tilldelar en samling av Hoare tripletter till varje förfarande; triples ger en över-uppskattning av datastruktur användning. Kompositionalitet ger sina vanliga fördelar -ökad potential att skala, förmåga att hantera okända kalla sammanhang, graciöst sätt att hantera imprecision - att forma analys, för första gången. Analysen bygger på en generaliserad form av bortförande (slutsatser av förklarande hypoteser) som vi kallar bi-abduction. Biabduction visar bortförande som ett slags invers till ram problemet: det gemensamt infer anti-frames (missing portions of state) och ramar (portioner av stat som inte berörs av en operation), och är grunden för en ny interprocedural analys algoritm. Vi har implementerat vår analysalgoritm och vi rapporterar fallstudier på mindre program för att utvärdera kvaliteten på upptäckta specifikationer, och större program (t.ex. en hel Linuxdistribution) för att testa skalbarhet och graciös imprecision.
Kompositionsform analyser baserade på biabduktion och separation logik har en hög potential att skala som visas i REF.
Compositional shape analysis by means of bi-abduction
{'venue': "POPL '09", 'journal': None, 'mag_field_of_study': ['Computer Science']}