Deep and Scalable Software Checking

丹尼尔·杰克逊，MIT深度和可伸缩软件检查软件在民用基础设施中的作用越来越大，软件故障带来的潜在巨大成本使可靠的软件成为迫切需要。开发可靠软件的技术将在未来几十年对美国经济至关重要。该项目正在开发一种新的检查软件的方法，以确保它具有所需的高级属性。在工业中，有两种技术被广泛使用：测试和静态分析(例如类型检查)，前者无法实现足够的覆盖率以找到导致低概率故障的缺陷，后者通常只能处理非常有限的属性，例如缺少某些类型的溢出或异常。在研究中，人们对能够找到最细微缺陷的更深层次的技术重新产生了兴趣，从而极大地增加了开发人员对代码正确性的信心。不幸的是，它们往往是不可伸缩的，因为它们通常需要比经济上更多的资源(无论是在计算上还是在人力上)。这个项目正在探索一种既保证深度又保证可伸缩性的新方法，在这种方法中，不是针对每种可能的情况(这似乎会导致可伸缩性问题)检查程序，而是对某些有限范围内的每种情况进行检查。关键思想是生成一个逻辑公式(代表代码的行为)，并用与约束求解器类似的公式(描述未能满足所需属性的特征)来表示它，然后约束求解器使用强大的搜索技术来探索那些可能导致失败的潜在执行的巨大空间。

ABSTRACTCCF-0541183PI: Daniel Jackson, MITDeep and Scalable Software CheckingThe growing role of software in civic infrastructure and the potentially huge costs of software failure make dependable software a pressing need. Technology for developing dependable software will be vital to the US economy in the coming decades.This project is developing a new approach for checking software to ensure that it has the desired high-level properties. In industry, two techniques are widely used: testing, which cannot achieve sufficient coverage to find the defects responsible for low-probability failures, and static analysis (such as type checking), which can typically handle only very limited properties, such as the absence of certain kinds of overflow or exception. In research, there has been a renewed interest in deeper techniques that are capable of finding the most subtle defects and thus dramatically increasing the developer's confidence in the correctness of the code. Unfortunately, these have tended not be scalable, since they often require more resources (either in computation or in human effort) than is economical. This project is exploring a new approach that promises both depth and scalability, in which a program is checked not for every possible case (which seems to lead to scalability problems), but rather for every case within some finite bounds. The key idea is to generate a logical formula (representing the behaviours of the code), and to present it with a similar formula (characterizing failure to satisfy a required property) to a constraint solver, which then uses powerful search techniques to explore a huge space of potential executions for those that would result in failures.