I næsten 40 år har dataloger arbejdet på at verificere egenskaber ved software matematisk. På trods af omfattende forskning på området kan de fleste værktøjer i praksis dog stadig kun verificere simple egenskaber. Det har i særdeleshed vist sig vanskeligt at udvikle værktøjer til verificering af ikke-triviale egenskaber ved programmer, der bygger på referencer til ”shared mutable” data, ”ubiquitous” i moderne objekt-orienterede programmeringssprog. Konsekvensen er, at de eksisterende værktøjer kun vil kunne fungere på små programmer.

Formålet med dette projekt er at undersøge og udvikle teorier og metoder til modulært ræsonnement om software skrevet i moderne programmeringssprog. Målet er at skabe et fundament for at kunne forbedre de softwareværktøjer, som er ved at blive udviklet nu og vil blive det i løbet af de næste fem til ti år, og som vil blive anvendt til at forbedre brugen af software. Løsningen af dette problem er af stor samfundsmæssig værdi, da fejl i software er ekstremt kostbare og kan have fatale konsekvenser.