cs.ru.nl Open in urlscan Pro
131.174.9.227  Public Scan

Form analysis
0 forms found in the DOM

Text Content

MARC SCHOOLDERMAN

--------------------------------------------------------------------------------

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.


CONTACT INFO

ln.ur.sc@namredloohcS.M
F290 176C 0550 EB80
Faculty of Science, Room M1.05.06, Toernooiveld 212, 6525EC Nijmegen


PUBLICATIONS

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


TEACHING

 * 2122 Software Development Management
 * 2122 Software Engineering
 * 2122 Functional Programming
 * 1819 Software Analysis
 * 1819 Software Engineering (Open University)
 * 1819 Mathematical Structures
 * 1718 Semantics & Correctness
 * 1718 Mathematical Structures
 * 1617 Mathematical Structures
 * 1516 Mathematical Structures
 * 1415 Combinatorics
 * 1415 Mathematical Structures


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


RESOURCES

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.

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

This homepage is written in Markdown.

--------------------------------------------------------------------------------