Model-finders, such as SAT/SMT-solvers and Alloy, are used widely both directly and embedded in domain-specific tools. They support both conventional verification and, unlike other verification tools, property-free exploration. To do this effectively, they must produce output that helps users with these tasks. Unfortunately, the output of model-finders has seen relatively little rigorous human-factors study. Conventionally, these tools tend to show one satisfying instance at a time. Drawing inspiration from the cognitive science literature, we investigate two aspects of model-finder output: how many instances to show at once, and whether all instances must actually satisfy the input constraints. Using both controlled studies and open-ended talk-alouds, we show that there is benefit to showing negative instances in certain settings; the impact of multiple instances is less clear. Our work is a first step in a theoretically grounded approach to understanding how users engage cognitively with model-finder output, and how those tools might better support users in doing so.

@article{paperbot1533,
  title = {Applying cognitive principles to model-finding output: the positive value of negative information},
  author = {Tristan Dyer and Tim Nelson and Kathi Fisler and Shriram Krishnamurthi},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {OOPSLA1},
  year = {2022},
  doi = {10.1145/3527323}
}