Abstrakt. Statiska analyser av objektorienterade program är vanligtvis beroende av mellanliggande representationer som respekterar de ursprungliga semantikerna samtidigt som de har en mer enhetlig och grundläggande syntax. Merparten av arbetet med objektorienterade språk och abstrakt tolkning utelämnar oftast beskrivningen av det språket eller hänvisar bara till Control Flow Graph (CFG) som det representerar. Men, denna brist på formalisering å ena sidan resulterar i en brist på försäkringar om riktigheten i omvandlingen och å andra sidan det typiskt starkt par analysen till källspråket. I detta arbete presenterar vi en ram för analys av objektorienterade språk där vi i en första fas omvandlar inmatningsprogrammet till en representation baserad på Hornklausuler. Detta gör det möjligt å ena sidan att bevisa omvandlingen korrekt att delta i ett enkelt tillstånd och å andra sidan att kunna tillämpa en befintlig analysator för (konstraint) logik programmering för att automatiskt härleda en säker approximation av semantiken i det ursprungliga programmet. Tillvägagångssättet är flexibelt i den meningen att den första fasen frikopplar analysatorn från de flesta språkberoende funktioner, och korrekt eftersom uppsättningen Horn klausuler returneras av omvandlingsfasen säkert approximerar standard semantik av inmatningsprogrammet. Den resulterande analysen är också någorlunda skalbar på grund av användningen av mogna, modulära (C)LP-baserade analysatorer. Den övergripande strategin gör det möjligt för oss att rapportera resultat för medelstora program.
Användningen av Hornklausuler som mellanliggande representation för kontroll föreslogs i REF.
A Flexible (C)LP-Based Approach to the Analysis of Object-Oriented Programs
{'venue': 'In 17th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR’07', 'journal': None, 'mag_field_of_study': ['Computer Science']}