Behovet for korrekt og pålidelig software præger alle dele af samfundet – fra telekommunikation, fabrikationsvirksomhed, handels- og finanssektoren til forsvaret og forskningsverdenen. Softwarekorrekted har mange facetter (usability, sikkerhed m.m.), men dette projekt fokusere på et andet aspekt, nemlig funktionskorrektheden for sekventielle programmer.

Udviklingen i de seneste 50 år har vist hvor svært det er at konstruere software, som fungerer korrekt. I løbet af de sidste 40 år har forskere forsøgt at udvikle programlogikker til formel specifikation og bevisførelse for softwarekorrekthed.
Såkaldte delte opdaterbare datastrukturer, der gennemsyrer moderne programmeringssprog som Java og C#, har vist sig at være særligt problematiske. Det er svært at udtrykke funktionelle egenskaber ved en sådan software og også at gennemføre beviser om dem.
I løbet af de seneste år er der gjort fremskridt på to fronter, nemlig i udviklingen af programlogik, særligt ”separation logic”, og i udviklingen af bevisværktøjer. Med ”separation logic” kan man fokusere et bevis på relevante delstrukturer af opdaterbare datastrukturer, men indtil videre har ”separation logic” kun været anvendt på mindre eksempler.

Projektets mål er derfor:

• At anvende de nævnte teoretiske landvindinger i praksis


• At konstruere prototyper af softwareværktøjer til formel specifikation med ”separation logic”


• At afprøve prototypen på et realistisk case study


• At levere metodiske anvisninger på softwarekonstruktion, så det bliver nemmere at formulere og vise egenskaber, og at rådgive om, hvordan sådanne beviser gennemføres