Wiskundige controle van populaire programmeertaal C (Promotie) - Radboud Universiteit

dinsdag 1 december 2015

Tijd

vanaf 10:30

Locatie

Senaatszaal Aula, Comeniuslaan 2

Faculteit

Faculteit der Natuurwetenschappen, Wiskunde en Informatica

Promovendus

de heer drs. R.J. Krebbers

Promotor(es)

prof. dr. J.H. Geuvers

Copromotor(es)

dr. F. Wiedijk

Subtitel

The C standard formalized in Coq

Beschrijving

Door programmeerfouten loopt software vast of krijgen de verkeerde mensen toegang tot vertrouwelijke informatie. Veel software is geschreven in de programmeertaal C en uitbreidingen daarvan, terwijl C een van de meest onveilige programmeertalen is. Daarom is er grote behoefte aan een manier om C-software te controleren op fouten.

In zijn proefschrift beschrijft Robbert Krebbers een zogenaamde formele specificatie, een wiskundige controle die het mogelijk maakt om met hoge zekerheid vast te stellen dat C-software correct functioneert. Met zijn onderzoek laat Krebbers zien dat zijn formele specificatie van programmeertaal C aan belangrijke wiskundige eisen voldoet.

Biografie

Robbert Krebbers (Groesbeek, 1987) studeerde Informatica aan de Radboud Universiteit en behaalde zowel zijn Bachelor- als zijn Masterdiploma cum laude. Tussen 2010 en 2011 werkte hij als junior onderzoeker bij het Formath project van de Europese Unie, later in 2011 begon hij aan zijn promotieonderzoek aan de Radboud Universiteit. Momenteel werkt Krebbers als postdoc onderzoeker bij de Aarhus Universiteit in Denemarken.