Applying formal verification to microkernel IPC at meta

Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli. Applying formal verification to microkernel IPC at meta. In Andrei Popescu 0001, Steve Zdancewic, editors, CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022. pages 116-129, ACM, 2022. [doi]

@inproceedings{CarbonneauxZKON22,
  title = {Applying formal verification to microkernel IPC at meta},
  author = {Quentin Carbonneaux and Noam Zilberstein and Christoph Klee and Peter W. O'Hearn and Francesco Zappa Nardelli},
  year = {2022},
  doi = {10.1145/3497775.3503681},
  url = {https://doi.org/10.1145/3497775.3503681},
  researchr = {https://researchr.org/publication/CarbonneauxZKON22},
  cites = {0},
  citedby = {0},
  pages = {116-129},
  booktitle = {CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
  editor = {Andrei Popescu 0001 and Steve Zdancewic},
  publisher = {ACM},
  isbn = {978-1-4503-9182-5},
}