‘Onzekere software’ voorspelbaar maken

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. 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. Een hypermoderne computer heeft bijvoorbeeld moeite met het verifiëren van de elementaire vraag: "stopt het programma überhaupt?"

Formele programmaverificatie- een set van regels om aan programma’s te rekenen – is een techniek die een programmeur goed helpt bij het vaststellen van de correcte werking. Probabilistische programma’s zijn echter lastiger te doorgronden, omdat ze omgaan met onzekere data en real-world observaties. Hoe kun je nog een conclusie trekken over de correcte werking als je je moet baseren op statistische gegevens over deze onzekere data?

Veiligheid

"Simulatietechnieken schieten uitgerekend tekort als het moeilijk wordt, in extreme situaties", aldus 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 dé 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."

Toch voorspelbaar

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. Probabilistisch programmeren gaat nadrukkelijk niet over software die zich ‘random’ gedraagt. Katoen: "Formele verificatie gaat het voorspelbaar maken".