SHF:Small:The Power of ``Why?'': Using Provenance for Disciplined Exploration in Model Finding

软件的可靠性在现代生活中变得越来越重要。电网、我们驾驶的汽车、我们的医院，甚至我们的食品生产，都严重依赖软件的运作。错误的风险可以通过被称为模型查找器的工具来降低，模型查找器可以产生具体的示例来帮助软件开发人员理解他们的系统。然而，大多数此类工具都存在这样的原则，即您得到的正是您所要求的，但有时并不是您真正想要或需要的。该项目致力于通过增加模型查找工具的解释力和改进示例的表示来提高模型查找工具的有效性。该项目开发的工具将适用于广泛的用户和领域，包括正规方法教育。这个项目探索了一种独特的模型搜索和证明搜索的融合，这是迄今为止尚未探索的。本项目的贡献包括：(1)在具有传递闭包的一阶逻辑中找到模型的明确定义的“这个必须在这里吗？”和“为什么在这里？”的概念，以及回答这些问题的算法；(2)基于其他形式方法子领域的覆盖概念，在模型之间导航和选择要呈现的模型的新方法；(3)对广泛使用的Alloy Analyzer进行扩展，实现这些想法并使其可供社区使用。

Software reliability is increasingly vital in modern life. The power grid, the cars we drive, our hospitals, and even our food production rely heavily on software to function. The risk of errors can be mitigated by tools, called model finders, that produce concrete examples to help software developers understand their system. However, most such tools suffer from the principle that you get precisely what you ask for, but sometimes not what you really want or need. This project works to improve the effectiveness of model-finding tools, both by increasing their explanatory power and improving presentation of examples. The tools developed in the project will be applicable to a wide range of users and domains, including formal-methods education.This project explores a unique melding of model-search and proof-search that has henceforth been unexplored. The contributions of this project include: (1) well defined notions of "Must this be here?" and "Why is this here?" for model finding in first-order logic with transitive closure, along with algorithms for answering these questions; (2) novel approaches to navigating between models and selecting which models to present, based on the concept of coverage from other formal methods sub-fields; and (3) extensions to the widely-used Alloy Analyzer that realize these ideas and make them available to the community.