摘要 : The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved s... 展开
作者 | Qinxiang Cao Lennart Beringer Samuel Gruetter Josiah Dodds Andrew W. Appel |
---|---|
作者单位 | |
期刊名称 | 《Journal of Automated Reasoning》 |
页码/总页数 | 367-422 / 56 |
语种/中图分类号 | 英语 / TP3 |
关键词 | Separation logic Symbolic execution Program verification Proof automation |
DOI | 10.1007/s10817-018-9457-5 |
馆藏号 | TP-148 |