Dead variable analysis for multi-threaded heap manipulating programs.
SAC 2016: Symposium on Applied Computing Pisa Italy April, 2016(2016)
摘要
Dead variable reduction is a well-known optimization used to reduce state space. In this paper we present two novel reductions for explicit-state code model checking. These reductions are designed to efficiently handle multi-threaded heap-manipulating programs. We implemented the reductions in Java PathFinder and demonstrated their efficiency by verification of several non-trivial programs. We also formally show correctness of the approach.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要