Marc Schoolderman

I am a teacher in the Digital Security group, and a PhD student in software verification, with a focus on using artificial intelligence to perform proofs.

Between 2016 and 2020 I worked in the Sovereign project (funded by NWO/TTW), which investigated the application of formal verification to security-critical systems. From 2020-2021 I was was a researcher for the LUCE project (funded by DARPA), which investigates automatic reasoning about memory bugs.

I am interested in proving useful properties about realistic applications; specifications that are human-readable but machine-verified; and incorporating practical know-how from industry. My current academic interests are systems for automated reasoning (such as Why3, CVC4, Z3), interactive provers (such as LEAN, Coq and PVS), embedded software, and domain specific languages.

Contact info
F290 176C 0550 EB80
Faculty of Science, Room M1.05.06, Toernooiveld 212, 6525EC Nijmegen


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


Students supervised

Jonathan Moerman (2020),
Asm3: modelling assembly languages efficiently in Why3,
MSc internship (thesis supervised by Freek Wiedijk)

Nienke Wessel (2019),
The Semantics of Ownership and Borrowing in the Rust Programming Language,
BSc thesis, co-supervised with Freek Wiedijk

Jonathan Moerman (2018),
Evaluating the performance of open source static analysis tools,
BSc thesis, second assessor (thesis supervised by Sjaak Smetsers)

Matthias Vogelaar (2017),
Defining the Undefined in C,
BSc thesis, co-supervised with Freek Wiedijk


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.

tinyTwofish, configurable implementation of the Twofish block cipher for AVR. Using the design as intended, can be used to get a very tiny or fast version, or a compromise between the two.

dunsel, a waste-basket for code of (at most) purely academic interest.

Non-peer-reviewed material

Verification of Goroutines using Why3,
MSc thesis, supervised by Freek Wiedijk.

Fuzzy Lexical Matching,
BSc thesis, supervised by Kees Koster.

An ALGOL-like imperative programming language, implemented as an embedded DSL using continuation-passing semantics inside Clean.

This homepage is written in Markdown.