@misc{indiciae3b1708e82f04, title = {A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability}, author = {Zheng Yang and Hang Lei}, year = {2018}, url = {https://arxiv.org/abs/1803.00403}, note = {Source identifier: 1803.00403} }