Deep and Scalable Software Checking

摘要CCF-0541183 PI：丹尼尔杰克逊，麻省理工学院深度和可扩展的软件检查软件在城市基础设施中日益增长的作用和软件故障的潜在巨大成本使可靠的软件成为迫切需要。开发可靠软件的技术对未来几十年的美国经济至关重要。该项目正在开发一种新的方法来检查软件，以确保它具有所需的高级属性。在工业中，有两种技术被广泛使用：测试，它不能达到足够的覆盖率来找到导致低概率故障的缺陷，以及静态分析（例如类型检查），它通常只能处理非常有限的属性，例如不存在某些类型的溢出或异常。在研究中，人们对更深入的技术重新产生了兴趣，这些技术能够发现最细微的缺陷，从而大大提高开发人员对代码正确性的信心。不幸的是，这些往往是不可扩展的，因为它们往往需要更多的资源（无论是在计算或人力）比经济。这个项目正在探索一种新的方法，它承诺深度和可扩展性，在这种方法中，程序不是针对每一种可能的情况（这似乎会导致可扩展性问题）进行检查，而是针对有限范围内的每一种情况。其关键思想是生成一个逻辑公式（表示代码的行为），并将其与一个类似的公式（描述未能满足所需属性的特征）一起呈现给约束求解器，然后约束求解器使用强大的搜索技术来探索可能导致失败的巨大执行空间。

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.