I am a PhD student in the Software Science group, interested in software verification, with a focus on using artificial intelligence to perform proofs.
Between 2016 and 2020 I worked in the Digital Security group for 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) at the Open University, investigating 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 academic interests are systems for automated reasoning (such as Why3, CVC4, Z3), secure programming, embedded software, and domain specific languages.
ln.ur.sc@namredloohcS.M
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
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.
Verification of Goroutines using Why3,
MSc thesis, supervised by Freek Wiedijk.
Fuzzy Lexical Matching,
BSc thesis, supervised by Kees Koster.
StdImperative
An ALGOL-like imperative programming language, implemented as an embedded DSL using continuation-passing semantics inside Clean.
This homepage is written in Markdown.