论文标题
在浮点程序中搜索反例时，带来可变选择的自由
Bringing freedom in variable choice when searching counter-examples in floating point programs
论文作者
论文摘要
程序验证技术通常集中于查找违反程序属性的反例。约束编程提供了一种方便的方式来通过建模其状态转换并指定寻求反例的搜索来验证程序。鉴于浮点算术的语义微妙，浮点计算给验证带来了其他挑战。 ％本文专注于使用浮点数限制系统的CSP搜索策略，并致力于程序验证。它基于超过最先进的策略的全球事件数量，引入了一种新的搜索启发式。更重要的是，它表明，仅在经过验证程序的输入变量上进行分支的新技术提高了性能。它由多元化技术组成，可防止在固定视野内选择相同变量的选择，从而进一步改善性能并减少各种可变选择启发式方法之间的差异。结果是一种强大的方法，可以根据反词示例的寻求特性来定制搜索策略。
Program verification techniques typically focus on finding counter-examples that violate properties of a program. Constraint programming offers a convenient way to verify programs by modeling their state transformations and specifying searches that seek counter-examples. Floating-point computations present additional challenges for verification given the semantic subtleties of floating point arithmetic. % This paper focuses on search strategies for CSPs using floating point numbers constraint systems and dedicated to program verification. It introduces a new search heuristic based on the global number of occurrences that outperforms state-of-the-art strategies. More importantly, it demonstrates that a new technique that only branches on input variables of the verified program improve performance. It composes with a diversification technique that prevents the selection of the same variable within a fixed horizon further improving performances and reduces disparities between various variable choice heuristics. The result is a robust methodology that can tailor the search strategy according to the sought properties of the counter example.
