Tools and Methods for Scalable Software Verifications

De sidste 50 år har vist at det er særdeles vanskeligt at konstruere software der fungerer korrekt. I 40 år har man forsøgt at udvikle programlogikker til formel specifikation og bevisførelse for softwarekorrekthed. Såkaldte delte opdaterbare

datastrukturer, der gennemsyrer moderne programmeringssprog såsom Java og C#, er særlig problematiske, både hvad angår at udtrykke funktionelle egenskaber og at gennemføre beviser om dem.



De seneste år er der gjort fremskridt i udviklingen af både programlogik og bevisværktøjer. Med separation logic, udviklet af Reynolds og O'Hearn, kan man fokusere et bevis på relevante delstrukturer, hvilket letter beskrivelse af delte

opdaterbare datastrukturer meget betydeligt. Imidlertid er separation logic indtil videre kun anvendt på mindre eksempler.



Måler med dette projekt er

(1) at bringe de nævnte teoretiske landvindinger nærmere til praksis,

(2) at konstruere prototyper af softwareværktøjer til formel specifikation med separation logic

(3) at afprøve prototypen på et realistisk case study

(4) at give metodiske anvisninger til softwarekonstruktion så det er nemmere at formulere og vise egenskaber.



Det påtænkte case study er et softwarebibliotek som er væsentligt fordi det bruges i praksis, udfordrende på grund af dets kompleksitet, og velegnet fordi dets struktur muliggør en trinvis tilgang til udfordringerne.



Projektet vil kombinere vores ekspertiser i moderne programmeringssprog og udviklingsmiljøer, og i det teoretiske grundlag for programlogik.