Modulaire formele verificatie van expressieve low-level objectgerichte programmeertalen

In dit doctoraatsonderzoek doen we onderzoek naar de theorie en aspecten bij het bouwen van tools, van het uitvoeren van modulaire formele verificatie van veiligheids- en beveiligingseigenschappen van programma's die geschreven zijn in programmeertalen die industrieel relevant zijn, zoals C++. Het doel hierbij is om de technologie van modulaire formele verificatie meer toepasbaar te maken in de industriële praktijk. Uitdagingen zijn onder meer het ondersteunen van C++ template en, de C++ Standerd Template Library, en het toevoegen van volledige ondersteuning voor het behandelen van structs of klassen als waarden, waarvoor nog geen goede ondersteuning bestaat door bestaande technologieën.