Efficient solving of structural constraints.
ISSTA(2008)
摘要
ABSTRACTStructural constraint solving is being increasingly used for software reliability tasks such as systematic testing or error recovery. For example, the Korat algorithm provides constraint-based test generation: given a Java predicate that describes desired input constraints and a bound on the input size, Korat systematically searches the bounded input space of the predicate to generate all inputs that satisfy the constraints. As another example, the STARC tool uses a constraint-based search to repair broken data structures. A key issue for these approaches is the efficiency of search. This paper presents a novel approach that significantly improves the efficiency of structural constraint solvers. Specifically, most existing approaches use backtracking through code re-execution to explore their search space. In contrast, our approach performs checkpoint-based backtracking by storing partial program states and performing abstract undo operations. The heart of our approach is a light-weight search that is performed purely through code instrumentation. The experimental results on Korat and STARC for generating and repairing a set of complex data structures show an order to two orders of magnitude speed-up over the traditionally used searches.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要