| CARVIEW |
Hey! I was a PhD student at Radboud University Nijmegen, supervised by
Robbert Krebbers
and
Herman Geuvers.
Starting March 17th, I will join the Automated Reasoning Group at Amazon Web Services as an Applied Scientist in Cambridge, UK.
My research interests include formalized mathematics, formal software verification and (proof) automation.
News
-
Our paper A Proof Recipe for Linearizability in Relaxed Memory Separation Logic was accepted at PLDI '24!
PDF ACM DL artifact -
Our paper Unification for Subformula Linking under Quantifiers was accepted at CPP '24!
PDF ACM DL iFrame MR artifact - We received a Distinguished Artifact Award for our OOPSLA '23 paper!
- I gave a talk at PLNL 2023, title: Proof Automation for Disjunctions in Concurrent Separation Logic. slides
- I gave a talk at the third edition of the Iris Workshop, titled: Proof Automation for Disjunctions and Logical Atomicity in Iris. slides
-
Our paper Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic was accepted at PLDI '23!
PDF ACM DL Coq development artifact -
Our paper Proof Automation For Linearizability in Separation Logic was accepted at OOPSLA '23!
PDF ACM DL Coq development artifact -
I gave an invited talk at the second edition of the Iris Workshop,
titled: Automating your Iris proofs with Diaframe.
slides demo files -
Our paper Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris was accepted at PLDI '22!
PDF ACM DL Coq development artifact
Diaframe
My PhD research project was centered around the development of Diaframe, a plugin for Iris aimed at (partially) automating proofs. Don't hesitate to reach out if you have questions!
Thesis
I defended my thesis on the 3rd of February 2025, and received a 'cum laude' distinction.
Publications
-
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers and Jeehoon Kang.
PDF
PLDI '24
-
Unification for Subformula Linking under Quantifiers
Ike Mulder and Robbert Krebbers.
PDF
CPP '24
-
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
Ike Mulder, Łukasz Czajka and Robbert Krebbers.
PDF
PLDI '23
-
Proof Automation For Linearizability in Separation Logic
Ike Mulder and Robbert Krebbers.
PDF
Distinguished artifact
OOPSLA '23
-
Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
Ike Mulder, Robbert Krebbers and Herman Geuvers.
PDF
PLDI '22
Other interests
I enjoy skiing, snowboarding and playing boardgames.