{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:37:39Z","timestamp":1791459459334,"version":"4.3.4"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"U.S. National Science Foundation","doi-asserted-by":"crossref","award":["1714431"],"award-info":[{"award-number":["1714431"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"crossref"}]},{"name":"U.S. DARPA","award":["2018-0047"],"award-info":[{"award-number":["2018-0047"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/3527323","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Applying cognitive principles to model-finding output: the positive value of negative information"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9730-9319","authenticated-orcid":false,"given":"Tristan","family":"Dyer","sequence":"first","affiliation":[{"name":"Brown University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9377-9943","authenticated-orcid":false,"given":"Tim","family":"Nelson","sequence":"additional","affiliation":[{"name":"Brown University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7895-8206","authenticated-orcid":false,"given":"Kathi","family":"Fisler","sequence":"additional","affiliation":[{"name":"Brown University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5184-1975","authenticated-orcid":false,"given":"Shriram","family":"Krishnamurthi","sequence":"additional","affiliation":[{"name":"Brown University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.27"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1080\/00461520.2013.775712"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.3102\/00346543070002181"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_14"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1037\/0278-7393.13.4.640"},{"key":"e_1_2_1_8_1","unstructured":"R. Brown and C. Hanlon. 1970. Derivational complexity and order of acquisition on child speech. In Cognition and the development of language J. Hayes (Ed.). Wiley. isbn:978-0471364733  R. Brown and C. Hanlon. 1970. Derivational complexity and order of acquisition on child speech. In Cognition and the development of language J. Hayes (Ed.). Wiley. isbn:978-0471364733"},{"key":"e_1_2_1_9_1","unstructured":"Fran\u00e7ois Chollet. 2019. On the Measure of Intelligence. arxiv:1911.01547.  Fran\u00e7ois Chollet. 2019. On the Measure of Intelligence. arxiv:1911.01547."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48077-6_3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592781"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1177\/001316446002000104"},{"key":"e_1_2_1_13_1","volume-title":"The Adapted Mind: Evolutionary Psychology and the Generation of Culture, Leda Cosmides, John Tooby, and Jerome H","author":"Cosmides Leda","year":"1951","unstructured":"Leda Cosmides and John Tooby . 1992. Cognitive Adaptions for Social Exchange . In The Adapted Mind: Evolutionary Psychology and the Generation of Culture, Leda Cosmides, John Tooby, and Jerome H . Barkow (Eds.). Oxford University Press . isbn:978-0 1951 01072 Leda Cosmides and John Tooby. 1992. Cognitive Adaptions for Social Exchange. In The Adapted Mind: Evolutionary Psychology and the Generation of Culture, Leda Cosmides, John Tooby, and Jerome H. Barkow (Eds.). Oxford University Press. isbn:978-0195101072"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54804-8_2"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66197-1_11"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1955.10501294"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-77543-8_7"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6370152"},{"key":"e_1_2_1_20_1","unstructured":"Ari Fogel Stanley Fung Luis Pedrosa Meg Walraed-Sullivan Ramesh Govindan Ratul Mahajan and Todd Millstein. 2015. A General Approach to Network Configuration Analysis. In Networked Systems Design and Implementation. 469\u2013483. isbn:978-1-931971-218 https:\/\/doi.org\/10.5555\/2789770.2789803  Ari Fogel Stanley Fung Luis Pedrosa Meg Walraed-Sullivan Ramesh Govindan Ratul Mahajan and Todd Millstein. 2015. A General Approach to Network Configuration Analysis. In Networked Systems Design and Implementation. 469\u2013483. isbn:978-1-931971-218 https:\/\/doi.org\/10.5555\/2789770.2789803"},{"key":"e_1_2_1_21_1","unstructured":"Eleanor J. Gibson. 1969. Principles of Perceptual Learning and Development. Appleton-Century-Crofts. isbn:9780390361455  Eleanor J. Gibson. 1969. Principles of Perceptual Learning and Development. Appleton-Century-Crofts. isbn:9780390361455"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1037\/h0048826"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1037\/h0084333"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10339-008-0243-x"},{"key":"e_1_2_1_25_1","volume-title":"Statistics","author":"Hays William L.","unstructured":"William L. Hays . 1994. Statistics ( 5 th ed.). Harcourt Brace College Publishers , Fort Worth . isbn:0030744679 William L. Hays. 1994. Statistics (5th ed.). Harcourt Brace College Publishers, Fort Worth. isbn:0030744679","edition":"5"},{"key":"e_1_2_1_26_1","volume-title":"Software Abstractions: Logic, Language, and Analysis (2 ed.)","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson . 2012 . Software Abstractions: Logic, Language, and Analysis (2 ed.) . MIT Press . isbn:0262017156 https:\/\/doi.org\/10.5555\/2141100 Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis (2 ed.). MIT Press. isbn:0262017156 https:\/\/doi.org\/10.5555\/2141100"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1357054.1357127"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-01303-9_4"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11858-017-0858-4"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46675-9_20"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_31"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24485-8_44"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0010-0277(93)90022-N"},{"key":"e_1_2_1_34_1","volume-title":"Necessary Conditions of Learning","author":"Marton Ference","unstructured":"Ference Marton . 2014. Necessary Conditions of Learning . Routledge . isbn:978-0415739146 Ference Marton. 2014. Necessary Conditions of Learning. Routledge. isbn:978-0415739146"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.14786\/flr.v1i1.16"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54494-5_2"},{"key":"e_1_2_1_37_1","volume-title":"The Margrave Tool for Firewall Analysis. In USENIX Large Installation System Administration Conference.","author":"Nelson Timothy","year":"2010","unstructured":"Timothy Nelson , Christopher Barratt , Daniel J. Dougherty , Kathi Fisler , and Shriram Krishnamurthi . 2010 . The Margrave Tool for Firewall Analysis. In USENIX Large Installation System Administration Conference. Timothy Nelson, Christopher Barratt, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. 2010. The Margrave Tool for Firewall Analysis. In USENIX Large Installation System Administration Conference."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_34"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1037\/0022-0663.99.3.561"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1037\/a0014224"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509584"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2491711"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_30"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1037\/a0025140"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951915"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91631-2_22"},{"key":"e_1_2_1_49_1","volume-title":"Human Reasoning and Cognitive Science","author":"Stenning Keith","year":"1958","unstructured":"Keith Stenning and Michiel van Lambalgen . 2008. Human Reasoning and Cognitive Science . MIT Press . isbn:9780262 1958 36 Keith Stenning and Michiel van Lambalgen. 2008. Human Reasoning and Cognitive Science. MIT Press. isbn:9780262195836"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1037\/h0054651"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2017.31"},{"key":"e_1_2_1_52_1","volume-title":"New Horizons in Psychology I","author":"Wason Peter Cathcart","year":"2077","unstructured":"Peter Cathcart Wason . 1966. Reasoning . In New Horizons in Psychology I , B. M. Foss (Ed.). Penguin . isbn:9780140 2077 50 Peter Cathcart Wason. 1966. Reasoning. In New Horizons in Psychology I, B. M. Foss (Ed.). Penguin. isbn:9780140207750"},{"key":"e_1_2_1_53_1","volume-title":"Learning Structural Descriptions from Examples","author":"Winston Patrick H.","unstructured":"Patrick H. Winston . 1970. Learning Structural Descriptions from Examples . Massachusetts Institute of Technology . Patrick H. Winston. 1970. Learning Structural Descriptions from Examples. Massachusetts Institute of Technology."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2019.00546"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527323","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527323","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527323"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":55,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527323"],"URL":"https:\/\/doi.org\/10.1145\/3527323","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}