A Verified Shared Capability Model

Electronic Notes in Theoretical Computer Science（2009）

引用 14|浏览1

暂无评分

摘要

This paper presents a methodology for automated modular verification of C programs against specifications written in separation logic. The distinguishing features of the approach are representation of the C memory model in separation logic by means of ...

查看译文

关键词

shared capabilities,distinguishing feature,automated modular verification,verified shared capability model,interactive theorem proving,c program,separation logic,c memory model,security policy

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要