Lazy Symbolic Execution For Enhanced Learning
RUNTIME VERIFICATION, RV 2014(2014)
摘要
The performance of symbolic execution based verifiers relies heavily on the quality of "interpolants", formulas which succinctly describe a generalization of states proven safe so far. By default, symbolic execution along a path stops the moment when infeasibility is detected in its path constraints, a property we call "eagerness". In this paper, we argue that eagerness may hinder the discovery of good quality inter-polants, and propose a systematic method that ignores the infeasibility in pursuit of better interpolants. We demonstrate with a state-of-the-art system on realistic benchmarks that this "lazy" symbolic execution outperforms its eager counterpart by a factor of two or more.
更多查看译文
关键词
Path Condition, Symbolic Execution, Feasible Path, Symbolic State, Program Point
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络