Formally verified superblock scheduling. - Cyril Six; Léo Gourdin; Sylvain Boulmé; David Monniaux; Justus Fasse; Nicolas Nardino (CPP, 2022)

Modular termination verification with a higher-order concurrent separation logic (Intermediate report). - Justus Fasse; Bart Jacobs 002 (CoRR, 2022)

Completeness Thresholds for Memory Safety of Array Traversing Programs. - Tobias Reinhard; Justus Fasse; Bart Jacobs 002 (SOAP@PLDI, 2023)

Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract). - Tobias Reinhard; Justus Fasse; Bart Jacobs 002 (CoRR, 2023)

Expressive modular verification of termination for busy-waiting programs. - Justus Fasse; Bart Jacobs 002 (CoRR, 2023)

An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (X)C20 memory consistency model. - Bart Jacobs 002; Justus Fasse (CoRR, 2025)