Managed hosting door True

2,5 miljoen naar UT-prof voor softwareonderzoek IoT

European Research Council stelt geld beschikbaar voor probabilistische programma’s

 

Zelfrijdende auto

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

"Katoen wil de techniek van ‘programmaverificatie’ ook geschikt maken voor probabilistische software."

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.

Dit artikel is afkomstig van Computable.nl (https://www.computable.nl/artikel/6335931). © Jaarbeurs IT Media.

?

 

Jouw reactie


Je bent niet ingelogd. Je kunt als gast reageren, maar dan wordt je reactie pas zichtbaar na goedkeuring door de redactie. Om je reactie direct geplaatst te krijgen, moet je eerst rechtsboven inloggen of je registreren

Je naam ontbreekt
Je e-mailadres ontbreekt
Je reactie ontbreekt

Stuur door

Stuur dit artikel door

Je naam ontbreekt
Je e-mailadres ontbreekt
De naam van de ontvanger ontbreekt
Het e-mailadres van de ontvanger ontbreekt

×
×
Wilt u dagelijks op de hoogte worden gehouden van het laatste ict-nieuws, achtergronden en opinie?
Abonneer uzelf op onze gratis nieuwsbrief.