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

SHF：小：“为什么？”的力量：在模型查找中使用来源进行严格的探索

• 批准号: 1714431
• 负责人: Shriram Krishnamurthi
• 金额: $ 45万
• 依托单位: Brown University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-07-01 至 2022-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1714431&HistoricalAwards=false
• 关键词: SHF; Small; Power; Why; Using

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.

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

项目成果

Who Tests the Testers? Avoiding the Perils of Automated Testing

谁来测试测试人员？

• DOI: 10.1145/3230977.3230999
• 发表时间: 2018
• 期刊: Proceedings of the 2018 ACM Conference on International Computing Education Research
• 作者: Wrenn, John;Krishnamurthi, Shriram;Fisler, Kathi
• 通讯作者: Fisler, Kathi

Automated, Targeted Testing of Property-Based Testing Predicates

基于属性的测试谓词的自动化、有针对性的测试

• DOI: 10.22152/programming-journal.org/2022/6/10
• 发表时间: 2021
• 期刊: and Engineering of Programming
• 作者: Nelson, Tim;Rivera, Elijah;Soucie, Sam;Del Vecchio, Thomas;Wrenn, John;Krishnamurthi, Shriram
• 通讯作者: Krishnamurthi, Shriram

Using Relational Problems to Teach Property-Based Testing

使用关系问题来教授基于属性的测试

• DOI: 10.22152/programming-journal.org/2021/5/9
• 发表时间: 2021
• 期刊: The art science and engineering of programming
• 作者: Wrenn, John;Nelson, Tim;and Krishnamurthi, Shriram
• 通讯作者: and Krishnamurthi, Shriram

CompoSAT: Specification-Guided Coverage for Model Finding

CompoSAT：规范指导的模型查找覆盖范围

• 发表时间: 2018
• 期刊: Lecture notes in computer science
• 作者: Porncharoenwase, Sorawee;Nelson, Tim;Krishnamurthi, Shriram
• 通讯作者: Krishnamurthi, Shriram

Solver-Aided Multi-Party Configuration

求解器辅助的多方配置

• DOI: 10.1145/3422604.3425944
• 发表时间: 2020
• 期刊: HotNets '20: Proceedings of the 19th ACM Workshop on Hot Topics in Networks
• 作者: Dackow, Kevin;Wagner, Andrew;Nelson, Tim;Krishnamurthi, Shriram;Benson, Theophilus A.
• 通讯作者: Benson, Theophilus A.