Mihir Parang Mehta, William R. Cook: Separation Logic-Based Verification Atop a Binary-Compatible Filesystem Model. SBMF 2020: 155-170