DrNLA：通过双重重写将验证扩展到非线性程序
摘要：将非线性整数算术（NLA）表达式的程序转换为语义等价的线性整数算术（LIA）程序的新方法：“双重重写”。通过双重重写技术，在NLA布尔表达式（例如在条件分支中找到的表达式）中发现线性替代，同时探索条件的正反两面，并使用静态验证和动态反例的一种组合。 由于NLA布尔表达式的真值可以用在表达式为真和表达式为假的区域/间隔的布尔组合方式来表征，因此将NLA表达式重写为LIA表达式能够使现有的LIA工具能够处理更广阔的NLA程序类。我们构建了一个名为DrNLA的新工具，并展示了它可以为各种NLA程序发现LIA替代方案。然后，我们将我们的工作应用于NLA程序的分支时间验证，创建了第一批这样的基准（总共92个），并展示了DrNLA的重写使得FuncTion和T2等工具能够验证以前无法验证的42个程序的CTL属性。我们还展示了DrNLA在辅助Frama-C程序切片方面的潜在用途，并报告了重写对执行速度影响不大。
作者：Yuandong Cyrus Liu, Ton-Chanh Le, Timos Antonopoulos, Eric Koskinen, ThanhVu Nguyen
论文ID：2306.15584
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-28