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

Brown University, Providence RI

Investigators

Abstract

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.