Hoe goed een bedrijf of een ontwikkelteam ook zijn best doet, alle software bevat fouten. Soms is het zo eenvoudig als een typefout ergens in een stuk code of twee puntkomma’s achter elkaar. Maar het probleem kan ook groter zijn. “Ik denk dat het door het gebruik van formele verificatietechnieken mogelijk is om veel fouten al vroeger te detecteren, en niet pas achteraf”, vertelt professor Marieke Huisman, hoogleraar in Software Reliability bij de Universiteit Twente. Huisman werkt met de Formal Methods and Tools Group van de universiteit aan verificatietechnieken voor software en hoopt deze naar de praktijk te brengen.

Met softwareverificatie wordt gekeken of software wel voldoet aan de eisen. Simpel gezegd: doet de software wat het moet doen, zonder dat er fouten plaatsvinden? Dit kan op twee manieren: dynamisch en statisch. Bij de dynamische variant wordt de software gecontroleerd tijdens het uitvoeren. Huisman richt zich met haar tool specifiek op statische verificatie, waarbij de verificatie plaatsvindt voordat de software uitgevoerd wordt.

Huisman heeft als doel om softwareverificatie bruikbaarder te maken voor ontwikkelaars en bedrijven. “Ik denk dat dit voor bedrijven heel interessant kan zijn, maar je ziet dat het nu echt nog heel veel tijd kost. Bovendien moet je hier best een expert voor zijn. Er is dus echt nog een slag te maken.”