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.

ln.ur.sc@namredloohcS.M

`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.

- 1819 Software Analysis
- 1718 Semantics & Correctness
- 1718 Mathematical Structures
- 1617 Mathematical Structures
- 1516 Mathematical Structures
- 1415 Combinatorics

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

Marc Schoolderman,

*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

StdImperative

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.