CAREER: Live Programming for Finite Model Finders

As software permeates every aspect of our everyday lives, the problem of software reliability has grown both in importance and complexity. Software modeling has shown promise in providing ways to improve software reliability, however the specialization required to build accurate software models has limited their adoption. Current model development environments are rather “bare bones,” providing no guidance or feedback other than the output itself, and limiting the revision process to the age-old “edit and check.” This project aims to address these challenges through the creation of a new model development environment. The project’s novelties are new tools that combine live programming innovations with the strengths inherent to modeling languages to provide a range of contextualized feedback during development. The project’s impacts are in lowering the barrier to entry for software modeling and aiding formal methods education. Concretely, this project focuses on bringing live programming to finite model finders to interweave the process of writing and evaluating a software model. To achieve this, the project investigates the efficacy of different live development interfaces that suggest edits to complete formulas and that help users explore and contrast how different edits impact the collection of scenarios produced. Since live programming elevates the role of the output, this project also explores a new model development workflow, output directed debugging, that enables users to edit the scenarios in order to correct the underlying model. In addition, these live interfaces will form the basis for an interactive learning environment for mathematical logic to improve formal methods education at both the undergraduate and graduate level. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.