Professor Joost-Pieter Katoen, hoogleraar aan de Rheinisch-Westfälische Technische Hochschule (RWTH) in Aken en de Universiteit Twente, krijgt een Advanced Grant van 2,5 miljoen euro van het European Research Council. Met dit geld gaat hij onderzoek doen naar zogenaamde ‘probabilistische’ computerprogramma’s. Deze software krijgt meer en meer te maken met onzekere IoT-data. Formele programmaverificatie is volgens Katoen de oplossing om de uitdagingen van het ‘omgaan met onzekere data’ het hoofd te bieden.
De tools die programmeurs normaal gesproken tot hun beschikking hebben om de correcte werking van software aan te tonen, zijn niet toereikend voor probabilistische software, zo meent de hoogleraar. Dat ligt niet aan de complexiteit van deze software, maar wel aan het omgaan met onzekerheid. Gebruikelijke software heeft al oneindig veel toestanden waarin het programma kan verkeren. Het doorrekenen hiervan is vrijwel onmogelijk. Formele programmaverificatie, een set van regels om aan programma’s te rekenen, is volgens hem een techniek die een programmeur wel goed helpt bij het vaststellen van de correcte werking van probabilistische software.
Geen simulatie maar verificatie
Simulatietechnieken schieten uitgerekend tekort als het moeilijk wordt in extreme situaties, aldus Joost-Pieter Katoen: ‘Je weet niet goed hoe lang je in zo’n geval moet doorgaan met simuleren, de simulaties geven bovendien geen harde garantie’. Volgens hem is formele verificatie de manier om deze tekortkomingen het hoofd te bieden. ‘Dat is een drastisch andere benadering, maar wel hard nodig in een tijd dat probabilistische software steeds vaker bepalend gaat worden voor bijvoorbeeld onze dagelijkse veiligheid. De zelfrijdende auto baseert er straks zijn beslissingen op’, aldus de professor.
Katoen wil de techniek van ‘programmaverificatie’ ook geschikt maken voor probabilistische software: deze techniek rekent aan software nog vóórdat het programma wordt uitgevoerd op een computer. Op die manier komen fouten en onverwacht gedrag aan het licht. Volgens katoen maakt formele verificatie de probalistische software voorspelbaar.
Profiel
Joost-Pieter Katoen is als hoogleraar verbonden aan de Rheinisch-Westfälische Technische Hochschule (RWTH) in Aken en aan de groep Formele Methoden en Technieken van de Universiteit Twente. Voor zijn project ‘FRAPPANT – Formal Reasoning About Probabilistic Programs – Breaking New Ground for Automation’ ontvangt hij een Advanced Grant van de European Research Council.
