Het bewijs van betrouwbare software bestaat
Als iemand met een pacemaker overlijdt, denkt de arts niet snel aan een deadlock in de pacemaker. Als een altijd trouw werkende brug opeens op hol slaat, wordt niet snel de link gelegd met een fundamentele fout in de besturingssoftware, die alleen problemen geeft doordat – in een uitzonderlijke situatie – twee conflicterende processen tegelijk starten. "Grote blunders ontdek je met reguliere testmethoden.
Maar ook daarna stikt software doorgaans nog van de fouten", stelt Jan Friso Groote, hoogleraar informatica aan de TU Eindhoven.