OSVAuto: automatic proofs about functional specifications in OS verification

Yulun Wu, Bican Xia, Jiale Xu +2

We present OSVAuto for automatic proofs about functional specifications that commonly arise when verifying operating system kernels. The algorithm behind OSVAuto is designed to sup…