Målene med denne workstream er:
- At udvikle stærke matematiske modeller og analyseværktøjer til verifikation af komplekse distribuerede softwaresystemer. Disse redskaber skal sikre, at alle aspekter ift. systemernes funktion, ressourceeffektivitet og sikkerhed afdækkes og analyseres.
- At udvikle og implementere understøttende verifikations- og analyseredskaber, der kan tilpasses den øgede kompleksitet i softwaresystemerne samt
- At sikre, at disse redskaber overføres til virksomheders udviklingspraksis.
Forskningen inden for verifikation og softwareudvikling supplerer og anvender teknikker fra andre forskningstemaer. Verifikation kan anvendes til at bevise sikkerhedsegenskaberne i Secure Multi-Party Computation og blockchains, jf. temaet Cybersikkerhed og blockchains, som Center for Program Verification allerede har demonstreret. Driftssikkerheden og robustheden i en lang række cyber-fysiske systemer og IoT-baserede systemer kan påvises ved hjælp af verifikations- og softwareudviklingsmetoder.
Kunstig intelligens anvendes i stigende grad til at accelerere og skalere eksisterende verifikationsteknikker. Maskinlæringskomponenter, herunder dybe neurale netværk, udfordrer eksisterende algoritmiske teknikker til verifikation, og der sker i øjeblikket spændene forskning inden for verificerbar og forklarlig kunstig intelligens.