@inproceedings{Andronick_LMMR_16,
    month            = aug,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9261.pdf},
    publisher        = {Springer},
    booktitle        = {International Conference on Interactive Theorem Proving},
    editor           = {{Jasmin Christian Blanchette and Stephan Merz}},
    author           = {Andronick, June and Lewis, Corey and Matichuk, Daniel and Morgan, Carroll and Rizkallah, Christine},
    year             = {2016},
    pages            = {52--68},
    title            = {Proof of {OS} scheduling behavior in the presence of interrupt-induced concurrency},
    address          = {Nancy, France}
  }