A Decision Procedure For An Extensional Theory Of Arrays

LICS '01: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science(2001)

引用 225|浏览302
暂无评分
摘要
A decision procedure for a theory of arrays is of interest for applications in formal verification, program analysis, and automated theorem-proving. This paper presents a decision procedure for an extensional theory of arrays and proves it correct.
更多
查看译文
关键词
arrays,data structures,decidability,formal verification,program diagnostics,theorem proving,array theory,automated theorem proving,correctness proof,decision procedure,extensional theory,formal verification,program analysis,
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要