Diaframe: automated verification of fine-grained concurrent programs in Iris. - Ike Mulder; Robbert Krebbers; Herman Geuvers (PLDI, 2022)

Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. - Ike Mulder; Lukasz Czajka 001; Robbert Krebbers (Proc. ACM Program. Lang., 2023)

Proof Automation for Linearizability in Separation Logic. - Ike Mulder; Robbert Krebbers (Proc. ACM Program. Lang., 2023)

Unification for Subformula Linking under Quantifiers. - Ike Mulder; Robbert Krebbers (CPP, 2024)

A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. - Sunho Park; Jaewoo Kim; Ike Mulder; Jaehwang Jung; Janggun Lee; Robbert Krebbers; Jeehoon Kang (Proc. ACM Program. Lang., 2024)