CAST: Tellerautomatenalgoritmes voor Softwareverificatietools. 01/10/2019 - 30/09/2023

Abstract

Formele verificatie van reactieve systemen is een steeds belangrijker onderzoeksgebied van informatica. Moderne systemen bevatten nu functies die hun ontwerp moeilijk maken en die ervoor zorgen dat het controleren van hun juistheid zeer veeleisend is. Bedrijven zoals Facebook en Amazon hebben teams die zich toeleggen op het formeel verifiëren van hun systemen, terwijl in de academische wereld de het werk op het gebied van verificatie in de afgelopen twintig jaar zijn geprezen met twee Turing-awards. Naarmate systemen complexer worden, zijn er meer ingewikkelde modellen nodig om hun gedrag vast te leggen. Tellerautomaten resulteren uit het toevoegen van geheel-getal waarde tellers aan het algemeen bestudeerde model van eindige automaten. De formele verificatiegemeenschap heeft verschillende toepassingen gevonden voor verschillende klassen van tellerautomaten. Dit project heeft tot doel (i) bij te dragen aan de theorie van automatische software verificatie --- model-checking van eentellerautomaten (ii) algoritmes voor model-checking te vertalen naar semi-beslissingsprocedures die implementeerbaar zijn in bestaande interactieve software verificatiehulpmiddelen en (iii) het sturen van de ontwikkeling van de theorie op basis van de beperkingen en mogelijkheden van dergelijke hulpmiddelen.

Onderzoeker(s)

Onderzoeksgroep(en)