De studerende vil kunne forstå og anvende basale program analyse formalismer og vil kunne konstruere og anvende analyse værktøjer og teknikker der understøttes af disse formalismer. En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:

• forklare de basale begreber introduceret i kurset;
• forklare konkrete analyser og deres anvendelse på simple programmer;
• forklare målet med analyse frameworks og deres instanser;
• formulere nye analyser som varianter af eksisterende analyser og kategorisere dem i de relevante analyse frameworks;
• forklare semantiske såvel som algoritmiske aspekter relateret til konkrete analyser;
• designe og konstruere et generisk software værktøj der understøtter analyser baseret på analyse frameworks;
• designe og motivere en sekvens af eksperimenter som benytter det konstruerede værktøj og kunne fortolke de opnåede resultater
• opnå ovennævnte resultater som del af et gruppe arbejde men på en sådan måde at de individuelle bidrag kan identificeres; og
• kommunikere de opnåede resultater på en klar og præcis måde i en standard form for teknisk rapport.

Kurset dække teknikker til dataflow analyse formuleret ved monotone frameworks. Dette involverer det teoretiske fundament inden for fix punkt teori såvel som forskellige algoritmiske tilgangsvinker til løsning af contraint systemer.

De studerende vil stifte bekendsskab med en række klassiske program analyser og vil som en del af kurset udvikle et mindre verifikationssystem til proaktiv analyse af et datasikkerheds problem. Kurset er baseret på "Principles of Program Analysis" af F. Nielson, H. Riis Nielson og C. Hankin (Springer, 2005, ISBN 3-540-65410-0). 04. maj, 2017