Applying formal verification to microkernel IPC at meta. - Quentin Carbonneaux; Noam Zilberstein; Christoph Klee; Peter W. O'Hearn; Francesco Zappa Nardelli (CPP, 2022)