User Evaluation Framework for Model Finding Research

We report the results of a series of crowd-sourced user studies in the formal-methods domain. Specifically, we explore the efficacy of the notion of minimal counterexample -- or more colloquially, minimal bug report -- when reasoning about logical specifications. Our results here suggest that minimal counterexamples are beneficial some specific cases, and harmful in others. Furthermore, our analysis leads to refined hypotheses about the role of minimal counterexamples that can be further evaluated in future studies. User-based evaluation has little precedent in the formal methods community. Therefore, as a further contribution, we discuss and analyze our research methodology, and offer guidelines for future user studies in formal methods research