I am a PhD student in the Digital Security group, working for the Sovereign project (funded by NWO/TTW), which aims to develop methods for the formal analysis of safety-critical systems.
For this project I am interested in proving safety properties of 'real world' software; building software that is safe by construction; and working with partners from industry in doing so. My current academic interests are systems for automated reasoning (such as Why3, ACL2 and PVS), as well as programming language design and domain specific languages.
F290 176C 0550 EB80
Faculty of Science, Room M1.01.01, Toernooiveld 212, 6525EC Nijmegen
bb-scripts, A set of bash-scripts for teaching assistants (and teachers) to make life working with Blackboard less painful.
fastavr, a simulator for Atmel's 8-bit AVR microcontrollers written in C and x86 assembly. Intended for testing and benchmarking AVR code efficiently.
dunsel, a waste-basket for code of (at most) purely academic interest.
Marc Schoolderman, Jonathan Moerman, Sjaak Smetsers, Marko van Eekelen,
Efficient Verification of Optimized Code: Correct High-speed Curve25519, NFM '21
Marc Schoolderman, Sjaak Smetsers, Marko van Eekelen,
Is Deductive Program Verification Mature Enough to be Taught to Software Engineers?, CSERC '19
Verifying Branch-Free Assembly Code in Why3, VSTTE '17
Marc Schoolderman, Rody Kersten, Jascha Neutelings, Marko van Eekelen,
ECAlogic: Hardware-Parametric Energy-Consumption Analysis of Algorithms, FOAL '14
An ALGOL-like imperative programming language, implemented as an embedded DSL using continuation-passing semantics inside Clean.
Verification of Goroutines using Why3,
MSc thesis, supervised by Freek Wiedijk.
Fuzzy Lexical Matching,
BSc thesis, supervised by Kees Koster.
This homepage is written in Markdown.